Institute of

Theoretical Computer Science

Carl-Friedrich-Gauß-Fakultät

Technische Universität Braunschweig

Publications by Roland Meyer

Publications by Roland Meyer

Recent

  1. Liveness Verification and Synthesis: New Algorithms for Recursive Programs, with Sebastian Muskalla and Elisabeth Neumann.

    arXiv

  2. Portability Analysis for Axiomatic Memory Models. PORTHOS: One Tool for all Models, with Hernan Ponce-de-Leon, Florian Furbach, and Keijo Heljanko.
    Accepted for SAS 2017.
    arXiv

  3. Domains for Higher-Order Games, with Matthew Hague and Sebastian Muskalla.
    Accepted for MFCS 2017.
    arXiv | Slides

  4. On the Upward/Downward Closures of Petri Nets, with Mohamed Faouzi Atig, Sebastian Muskalla, and Prakash Saivasan.
    Accepted for MFCS 2017.
    arXiv | Slides

  5. Munchausen Iteration, with Sebastian Muskalla.

    arXiv

  6. Inductive Counting and the Reachability Problem for Petri Nets, with Peter Chini.
    Accepted for Carl Adam Petri - His Ideas, Personality, and Impact: Personal Stories.

Conference contributions

  1. Effect Summaries for Thread-Modular Analysis, with Lukas Holik, Tomas Vojnar, and Sebastian Wolff.
    In Proceedings of SAS 2017.
    PDF | Slides | DOI | arXiv | Code on GitHub

  2. On the Complexity of Bounded Context Switching, with Peter Chini, Jonathan Kolberg, Andreas Krebs, and Prakash Saivasan.
    In Proceedings of ESA 2017.
    Conference Version | DOI/BibTex | Full Version @ arXiv

  3. Locality and Singularity for Store-Atomic Memory Models, with Egor Derevenetc and Sebastian Schweizer.
    In Proceedings of NETYS 2017.
    DOI | arXiv

  4. Summaries for Context-Free Games, with Lukas Holik and Sebastian Muskalla.
    In Proceedings of FSTTCS 2016.
    Conference Version | DOI/BibTex | Full Version @ arXiv | Slides (Conference Version) | Slides (Full Version)

  5. First-order logic with reachability for infinite-state systems, with Emanuele D'Osualdo and Georg Zetzsche.
    In Proceedings of LICS 2016.
    PDF | DOI

  6. Pointer Race Freedom, with Frederic Haziza, Lukas Holik, and Sebastian Wolff.
    In Proceedings of VMCAI 2016.
    PDF | DOI | BibTeX

  7. What's Decidable about Availability Languages?, with Parosh Abdulla, Mohamed Faouzi Atig, and Mehdi Seyed Salehi.
    In Proceedings of FSTTCS 2015.
    PDF | DOI | BibTeX

  8. Antichains for Recursive Program Verification, with Lukas Holik.
    In Proceedings of NETYS 2015.
    PDF | DOI | BibTeX

  9. Lazy TSO Reachability, with Ahmed Bouajjani, Georgel Calin, and Egor Derevenetc.
    In Proceedings of FASE 2015.
    arXiv | DOI | BibTeX

  10. From Program Verification to Time and Space: The Scientific Life of Ernst-Rüdiger Olderog, with Heike Wehrheim.
    In Proceedings of Symposium in Honor of Ernst-Rüdiger Olderog.
    DOI | BibTeX

  11. Bounds on Mobility, with Reiner Hüchting and Rupak Majumdar.
    In Proceedings of CONCUR 2014.
    PDF | DOI | BibTeX

  12. Robustness against Power is PSPACE-complete, with Egor Derevenetc.
    In Proceedings of ICALP 2014.
    arXiv | DOI | BibTeX

  13. Memory-Model-Aware Testing - a Unified Complexity Analysis, with Florian Furbach, Klaus Schneider, and Maximilian Senftleben.
    In Proceedings of ACSD 2014.

    ACSD 2014 best paper award.
    DOI | PDF

  14. Checking and Enforcing Robustness against Relaxed Memory Models, with Ahmed Bouajjani and Egor Derevenetc.
    In Proceedings of SE 2014.
    PDF

  15. A Theory of Name Boundedness, with Reiner Hüchting and Rupak Majumdar.
    In Proceedings of CONCUR 2013.
    PDF | DOI

  16. Provenance Verification, with Rupak Majumdar and Zilong Wang.
    In Proceedings of RP 2013.
    DOI | BibTeX

  17. A Theory of Partitioned Global Address Spaces, with Georgel Calin, Egor Derevenetc, and Rupak Majumdar.
    In Proceedings of FSTTCS 2013.
    arXiv | DOI | BibTeX

  18. Checking and Enforcing Robustness against TSO, with Ahmed Bouajjani and Egor Derevenetc.
    In Proceedings of ESOP 2013.
    PDF (full version) | DOI | BibTeX

  19. Static Provenance Verification for Message Passing Programs, with Rupak Majumdar and Zilong Wang.
    In Proceedings of SAS 2013.
    PDF | DOI | BibTeX

  20. A Polynomial Translation of Pi-Calculus (FCP) to Safe Petri Nets, with Victor Khomenko and Reiner Hüchting.
    In Proceedings of CONCUR 2012.
    PDF | DOI

  21. Language-Theoretic Abstraction Refinement, with Zhenyue Long, Georgel Calin, and Rupak Majumdar.
    In Proceedings of FASE 2012.

    ETAPS 2012 best paper award by EAPLS.
    DOI | www | BibTeX

  22. An Algorithmic Framework for Coverability in Well-Structured Systems, with Tim Strazny.
    In Proceedings of ACSD 2012.

    ACSD 2012 best paper award.
    DOI | BibTeX

  23. Deciding Robustness against Total Store Ordering, with Ahmed Bouajjani and Eike Möhlmann.
    In Proceedings of ICALP 2011.
    DOI | BibTeX

  24. Petri Net Reachability Graphs: Decidability Status of FO Properties, with Ph. Darondeau, S. Demri, and C. Morvan.
    In Proceedings of FSTTCS 2011.
    DOI | BibTeX

  25. Kleene, Rabin, and Scott are available, with Jochen Hoenicke and Ernst-Rüdiger Olderog.
    In Proceedings of CONCUR 2010.
    PDF | DOI | BibTeX

  26. The downward-closure of Petri net languages, with Peter Habermehl and Harro Wimmel.
    In Proceedings of ICALP 2010.
    Slides | PDF | DOI | BibTeX

  27. Petruchio: From dynamic networks to nets, with Tim Strazny.
    In Proceedings of CAV 2010.
    PDF | DOI | BibTeX

  28. Checking pi-calculus structural congruence is graph isomorphism complete, with Victor Khomenko.
    In Proceedings of ACSD 2009.
    DOI | PDF | BibTeX

  29. On the relationship between pi-calculus and finite place/transition Petri nets, with Roberto Gorrieri.
    In Proceedings of CONCUR 2009.
    Slides | PDF | DOI | BibTeX

  30. A practical approach to verification of mobile systems using net unfoldings, with Victor Khomenko and Tim Strazny.
    In Proceedings of PETRI NETS 2008.
    Slides | PDF | DOI | BibTeX

  31. On boundedness in depth in the pi-calculus.
    In Proceedings of IFIP TCS 2008.
    Slides | PDF | DOI | BibTeX

  32. Model checking data-dependent real-time properties of the European Train Control System, with Johannes Faber.
    In Proceedings of FMCAD 2006.
    DOI | BibTeX | Slides

  33. Model checking duration calculus: A practical approach, with Johannes Faber and Andrey Rybalchenko.
    In Proceedings of ICTAC 2006.
    PDF | DOI | BibTeX

  34. Compositional semantics for UML 2.0 sequence diagrams using Petri nets, with Christoph Eichner, Hans Fleischhack, Ulrik Schrimpf, and Christian Stehno.
    In Proceedings of SDL 2005.
    DOI | BibTeX

Editor

  1. Stefan Haar and Roland Meyer, editors. Special Issue on ACSD 2015, ACM Transactions on Embedded Computing Systems (TECS), 16(2). ACM, 2017.
    Webpage | BibTeX

  2. Roland Meyer and Uwe Nestmann, editors. Proceedings of the 28th International Conference on Concurrency Theory (CONCUR), Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017.
    Webpage | BibTeX

  3. Stefan Haar and Roland Meyer, editors. Proceedings of the 15th International Conference on Application of Concurrency to System Design (ACSD), IEEE Computer Society Press, 2015.
    Webpage | BibTeX

  4. Roland Meyer, Andre Platzer, and Heike Wehrheim, editors. Correct System Design: Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, Proceedings , 9360 of LNCS. Springer, 2015.
    DOI | BibTeX

  5. M. Diehl, H. Lipskoch, Roland Meyer, and C. Storm, editors. Proceedings des gemeinsamen Workshops der Graduiertenkollegs , 4 of Trustworthy Software Systems. GITO, 2008.

Journal articles

  1. Memory-Model-Aware Testing - a Unified Complexity Analysis, with Florian Furbach, Klaus Schneider, and Maximilian Senftleben.
    ACM Transactions on Embedded Computing Systems (TECS), 2015.
    PDF | BibTeX

  2. A Polynomial Translation of Pi-Calculus (FCP) to Safe Petri Nets, with Victor Khomenko and Reiner Hüchting.
    Logical Methods in Computer Science, 2013.
    arXiv | BibTeX

  3. Petri Net Reachability Graphs: Decidability Status of FO Properties, with Ph. Darondeau, S. Demri, and C. Morvan.
    Logical Methods in Computer Science, 2012.
    BibTeX

  4. A Theory of Structural Stationarity in the Pi-Calculus.
    Acta Informatica, 2009.
    DOI | BibTeX

  5. A Practical Approach to Verification of Mobile Systems using Net Unfoldings, with Victor Khomenko and Tim Strazny.
    Fundamenta Informaticae, 2009.
    DOI | BibTeX

  6. Model Checking Duration Calculus: A Practical Approach., with Johannes Faber, Jochen Hoenicke, and Andrey Rybalchenko.
    Formal Aspects of Computing, 2008.
    PDF | DOI | BibTeX

  7. Trustworthy Software Systems: A Discussion of Basic Concepts and Terminology., with S. Becker, W. Hasselbring, A. Paul, M. Boskovic, H. Koziolek, J. Ploski, A. Dhama, H. Lipskoch, M. Rohr, , S. Giesecke, M. Swaminathan, J. Happe, M. Muhle, and T. Warns.
    ACM SIGSOFT Software Engineering Notes, 2006.
    DOI | BibTeX

Workshop contributions

  1. Strukturelle Stationarität.
    In Ausgezeichnete Informatik Dissertationen, 2009.
    PDF, in German | BibTeX

  2. Automata-theoretic verification based on counterexample specifications, with Ernst-Rüdiger Olderog.
    In Informatik als Dialog zwischen Theorie und Anwendung, 2009.
    DOI | BibTeX

  3. A Petri net semantics for pi-calculus verification.
    In Dagstuhl "zehn plus eins", 2007.
    BibTeX

  4. Model checking the pi-calculus.
    In Proc. of the International Research Training Groups Workshop, 2006.
    BibTeX

Theses

  1. Structural Stationarity in the pi-Calculus. PhD thesis.
    Department of Computing Science, University of Oldenburg, 2009.
    Slides | PDF | BibTeX

  2. Model-Checking von Phasen-Event-Automaten bezüglich Duration Calculus Formeln mittels Testautomaten. Master's thesis.
    Department of Computing Science, University of Oldenburg, 2005.
    PDF, in German | BibTeX

Technical Reports

  1. A Polynomial Translation of Pi-Calculus (FCP) to Safe Petri Nets, with Victor Khomenko and Reiner Hüchting.
    Technical Report CS-TR-1323, School of Computing Science, Newcastle University, 2012.
    PDF

  2. Checking pi-calculus structural congruence is graph isomorphism complete, with Victor Khomenko.
    Technical Report CS-TR-1100, School of Computing Science, Newcastle University, 2008.
    PDF | BibTeX

  3. On depth and breadth in the pi-calculus.
    Technical Report 01/08, Department of Computing Science, University of Oldenburg, 2008.
    BibTeX

  4. A practical approach to verification of mobile systems using net unfoldings, with Victor Khomenko and Tim Strazny.
    Technical Report CS-TR-1064, School of Computing Science, Newcastle University, 2008.
    PDF | BibTeX