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. Munchausen Iteration, with Sebastian Muskalla.

    arXiv

  3. Fast Witness Counting, with Peter Chini, Rehab Massoud, and Prakash Saivasan.

    arXiv

Conference contributions

  1. Parameterized Verification under Release Acquire is PSPACE-complete, with Shankaranarayanan Krishna, Adwait Godbole, and Soham Chakraborty.
    In Proceedings of PODC 2022. To appear.

  2. Dartagnan: SMT-based Violation Witness Validation, with Hernan Ponce-de-Leon and Thomas Haas.
    In Proceedings of TACAS 2022. Competition Contribution (SVCOMP).
    PDF

  3. Model-Based Fault Classification for Automotive Software, with Sören van der Wall and Sebastian Wolff.
    In Proceedings of APLAS 2022.
    DOI

  4. Dartagnan: Leveraging Compiler Optimizations and the Price of Precision, with Hernan Ponce-de-Leon and Thomas Haas.
    In Proceedings of TACAS 2021. Competition Contribution (SVCOMP).

  5. Dartagnan: Bounded Model Checking for Weak Memory Models, with Hernan Ponce-de-Leon, Florian Furbach, and Keijo Heljanko.
    In Proceedings of TACAS 2020. Competition Contribution.
    PDF | Project Page | DOI | BibTeX

  6. On the Complexity of Multi-Pushdown Games, with Sören van der Wall.
    In Proceedings of FSTTCS 2020.
    DOI | PDF

  7. Safety Verification under Power, with Parosh Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Egor Derevenetc, and Carl Leonardsson.
    In Proceedings of NETYS 2020. To appear.
    DOI | BibTeX

  8. Pointer Life Cycle Types for Lock-Free Data Structures with Memory Reclamation, with Sebastian Wolff.
    In Proceedings of POPL 2020. Artifact evaluated: functional&reusable.
    PDF | Slides | Project Page | DOI | arXiv

  9. Sicherheit, Zuverlässigkeit, Korrektheit, with Juliane Krämer.
    In Proceedings of INFORMATIK 2019.
    DOI | BibTeX

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

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

  12. Complexity of Liveness in Parameterized Systems, with Peter Chini and Prakash Saivasan.
    In Proceedings of FSTTCS 2019.
    Conference Version | DOI/BibTex | Full Version @ arXiv

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    ACSD 2012 best paper award.
    DOI | BibTeX

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

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

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

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

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

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

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

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

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

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

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

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

  58. 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. Karima Echihabi and Roland Meyer, editors. Proceedings of the 09th International Conference on Networked Systems (NETYS), 12754 of LNCS. Springer, 2021.
    DOI | BibTeX

  2. Roland Meyer and Uwe Nestmann, editors. Selected Papers of the 28th International Conference on Concurrency Theory (CONCUR 2017), 15(3/4). Logical Methods in Computer Science (LMCS), 2019.
    Webpage | BibTeX

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

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

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

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

  7. 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. Liveness in Broadcast Networks, with Peter Chini and Prakash Saivasan.
    Computing, 2021.
    Conference Version | Full Version @ arXiv

  2. Fine-Grained Complexity of Safety Verification, with Peter Chini and Prakash Saivasan.
    Journal of Automated Reasoning, 2020.
    DOI | arXiv

  3. Fine-Grained Complexity of Program Verification Tasks, with Peter Chini and Prakash Saivasan.
    Parameterized Complexity Newsletter, 2019.
    PDF

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

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

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

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

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

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

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

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