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

Conference contributions

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    ACSD 2012 best paper award.
    DOI | BibTeX

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  6. 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 Theory of Structural Stationarity in the Pi-Calculus.
    Acta Informatica, 2009.
    DOI | BibTeX

  8. A Practical Approach to Verification of Mobile Systems using Net Unfoldings, with Victor Khomenko and Tim Strazny.
    Fundamenta Informaticae, 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. 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