My primary researching area is real-time model checking techniques with specific interests in discrete time properties and model transformation.
Most of my work is done in collaboration with my thesis advisor Professor Kim G. Larsen and Assosciate Professor Jiri Srba. As a part of my postgraduate work I was one of the creators of the model checking tool TAPAAL, for verification of Timed-Arc Petri Nets.

You can find me on DBLP and Google Scholar

Proceedings Publications

  • TAPAAL 2.0: Integrated Development Environment for Timed-Arc Petri Nets
    by A. David, L. Jacobsen, M. Jacobsen, K.Y. Jørgensen, M.H. Møller and J. Srba.

  • A Semantic-Preserving Transformation from the Compositional Interchange Format to UPPAAL
    by D.E. Nadales Agut, M.A. Reniers, R.R.H. Schiffelers, K.Y. Jørgensen, and D.A. van Beek.

  • opaal - A Lattice Model Checker
    by Andreas E. Dalsgaard, Rene R. Hansen, Kenneth Yrke Joergensen, Kim G. Larsen, Mads Chr. Olesen, Petur Olsen and Jiri Srba.

  • An Efficient Translation of Timed-Arc Petri Nets to Networks of Timed Automata
    by Joakim Byg, Kenneth Yrke Joergensen and Jiri Srba.

  • TAPAAL: Editor, Simulartor and Verifier of Timed-Arc Petri Nets
    by Joakim Byg, Kenneth Yrke Joergensen and Jiri Srba

Journal Publications

  • Pending Update

Book Chapters

  • Pending Update

Technical Publications

  • An Efficient Translation of Timed-Arc Petri Nets to Networks of Timed Automata
    by Joakim Byg, Kenneth Yrke Joergensen and Jiri Srba.Technical report FIMU-RS-2009-06 , Faculty of Informatics MU, 29 pages, 2009.

Master Thesis

  • Regular Model Checking and Verification of Cellular Automata
    by Joakim Byg and Kenneth Yrke Jørgensen.
    Department of Computer Science, Aalborg University. 2008.
    Supervisor: Jiri Srba.