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. Fast Witness Counting, with Peter Chini, Rehab Massoud, and Prakash Saivasan.

    arXiv

  3. Munchausen Iteration, with Sebastian Muskalla.

    arXiv

  4. Complexity of Liveness in Parameterized Systems, with Peter Chini and Prakash Saivasan.

    FSTTCS 2019

Conference contributions

  1. Decoupling Lock-Free Data Structures from Memory Reclamation for Static Analysis, with Sebastian Wolff.
    In Proceedings of POPL 2019. Artifact evaluated: functional&reusable.
    PDF | Slides | Project Page | DOI | arXiv

  2. Temporal Tracing of On-chip Signals using Timeprints, with Rehab Massoud, Peter Chini, Prakash Saivasan, Hoang M. Le, and Rolf Drechsler.
    In Proceedings of DAC 2019.
    PDF | DOI

  3. BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings, with Natalia Gavrilenko, Hernan Ponce-de-Leon, Florian Furbach, and Keijo Heljanko.
    In Proceedings of CAV 2019. Artifact evaluated positively.
    PDF | Project Page | CAV 2019 | DOI | BibTeX

  4. Liveness in Broadcast Networks, with Peter Chini and Prakash Saivasan.
    In Proceedings of NETYS 2019.

    Best Student Paper Award.
    Conference Version | DOI/BibTex | Full Version @ arXiv

  5. Inductive Counting and the Reachability Problem for Petri Nets , with Peter Chini.
    In Carl Adam Petri: Ideas, Personality, Impact, 2019.
    Book | DOI

  6. BMC with Memory Models as Modules, with Hernan Ponce-de-Leon, Florian Furbach, and Keijo Heljanko.
    In Proceedings of FMCAD 2018.
    PDF | BibTeX

  7. Bounded Context Switching for Valence Systems, with Sebastian Muskalla and Georg Zetzsche.
    In Proceedings of CONCUR 2018.
    PDF | DOI & BibTex | Full Version @ arXiv | Slides

  8. Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems, with Matthew Hague, Sebastian Muskalla, and Martin Zimmermann.
    In Proceedings of MFCS 2018.
    PDF | DOI & BibTex | Full Version @ arXiv | Slides

  9. Reasoning About Weak Semantics via Strong Semantics, with Sebastian Wolff.
    In Principled Software Development - Essays Dedicated to Arnd Poetzsch-Heffter on the Occasion of his 60th Birthday, 2018.
    PDF | Book | DOI

  10. Fine-Grained Complexity of Safety Verification, with Peter Chini and Prakash Saivasan.
    In Proceedings of TACAS 2018.
    Conference Version | DOI/BibTex | Full Version @ arXiv

  11. Regular Separability of Well-Structured Transition Systems, with Wojciech Czerwiński, Sławomir Lasota, Sebastian Muskalla, K Narayan Kumar, and Prakash Saivasan.
    In Proceedings of CONCUR 2018.
    PDF | DOI & BibTex | Full Version @ arXiv | Slides | Poster

  12. Portability Analysis for Axiomatic Memory Models. PORTHOS: One Tool for all Models, with Hernan Ponce-de-Leon, Florian Furbach, and Keijo Heljanko.
    In Proceedings of SAS 2017.
    DOI | arXiv

  13. Domains for Higher-Order Games, with Matthew Hague and Sebastian Muskalla.
    In Proceedings of MFCS 2017.
    PDF | DOI & BibTex | Full Version @ arXiv | Slides

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

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

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

  17. On the Upward/Downward Closures of Petri Nets, with Mohamed Faouzi Atig, Sebastian Muskalla, and Prakash Saivasan.
    In Proceedings of MFCS 2017.
    PDF | DOI & BibTex | Full Version @ arXiv | Slides

  18. Summaries for Context-Free Games, with Lukas Holik and Sebastian Muskalla.
    In Proceedings of FSTTCS 2016.
    PDF | DOI & BibTex | Full Version @ arXiv | Slides

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    ACSD 2012 best paper award.
    DOI | BibTeX

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

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

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

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

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

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

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

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

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

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

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

  48. 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. Fine-Grained Complexity of Program Verification Tasks, with Peter Chini and Prakash Saivasan.
    Parameterized Complexity Newsletter, 2019.
    PDF

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

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

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

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

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

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

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