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

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

  5. On the Complexity of Bounded Context Switching, with Peter Chini, Jonathan Kolberg, Andreas Krebs, and Prakash Saivasan.
    Accepted for ESA 2017.
    arXiv

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

  7. Munchausen Iteration, with Sebastian Muskalla.

    arXiv

  8. 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. Locality and Singularity for Store-Atomic Memory Models, with Egor Derevenetc and Sebastian Schweizer.
    In Proceedings of NETYS 2017.
    DOI | arXiv

  2. 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)

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

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

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

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

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

  8. 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

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

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

  11. 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

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

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

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

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

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

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

  18. 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

  19. 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

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

    ACSD 2012 best paper award.
    DOI | BibTeX

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

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

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

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

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

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

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

  28. 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

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

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

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

  32. 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. 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

  3. 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

  4. 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