Conference contributionsConference contributions
- Dartagnan: Leveraging Compiler Optimizations and the Price of Precision,
by Hernan Ponce-de-Leon, Thomas Haas, and Roland Meyer.
In Proceedings of TACAS 2021.
Competition Contribution (SVCOMP).
- Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games,
by Kittiphon Phalakarn, Toru Takisaka, Thomas Haas, and Ichiro Hasuo.
In Proceedings of CAV 2020.
DOI | arXiv
- Safety Verification under Power,
by Parosh Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Egor Derevenetc, Carl Leonardsson, and Roland Meyer.
In Proceedings of NETYS 2020.
To appear.
DOI | BibTeX
- Dartagnan: Bounded Model Checking for Weak Memory Models,
by Hernan Ponce-de-Leon, Florian Furbach, Keijo Heljanko, and Roland Meyer.
In Proceedings of TACAS 2020.
Competition Contribution.
PDF | Project Page | DOI | BibTeX
- Pointer Life Cycle Types for Lock-Free Data Structures with Memory Reclamation,
by Roland Meyer and Sebastian Wolff.
In Proceedings of POPL 2020.
Artifact evaluated: functional&reusable.
PDF | Slides | Project Page | DOI | arXiv
- A Framework for Consistency Algorithms,
by Peter Chini and Prakash Saivasan.
In Proceedings of FSTTCS 2020.
Conference Version | DOI/BibTex | Full Version @ arXiv
- On the Complexity of Multi-Pushdown Games,
by Roland Meyer and Sören van der Wall.
In Proceedings of FSTTCS 2020.
DOI | PDF
- Decoupling Lock-Free Data Structures from Memory Reclamation for Static Analysis,
by Roland Meyer and Sebastian Wolff.
In Proceedings of POPL 2019.
Artifact evaluated: functional&reusable.
PDF | Slides | Project Page | DOI | arXiv
- Complexity of Liveness in Parameterized Systems,
by Peter Chini, Roland Meyer, and Prakash Saivasan.
In Proceedings of FSTTCS 2019.
Conference Version | DOI/BibTex | Full Version @ arXiv
- Temporal Tracing of On-chip Signals using Timeprints,
by Rehab Massoud, Peter Chini, Prakash Saivasan, Roland Meyer, Hoang M. Le, and Rolf Drechsler.
In Proceedings of DAC 2019.
PDF | DOI
- Sicherheit, Zuverlässigkeit, Korrektheit,
by Juliane Krämer and Roland Meyer.
In Proceedings of INFORMATIK 2019.
DOI | BibTeX
- BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings,
by Natalia Gavrilenko, Hernan Ponce-de-Leon, Florian Furbach, Keijo Heljanko, and Roland Meyer.
In Proceedings of CAV 2019.
Artifact evaluated positively.
PDF | Project Page | CAV 2019 | DOI | BibTeX
- Liveness in Broadcast Networks,
by Peter Chini, Roland Meyer, and Prakash Saivasan.
In Proceedings of NETYS 2019.
Best Student Paper Award.
Conference Version | DOI/BibTex | Full Version @ arXiv
-
Inductive Counting and the Reachability Problem for Petri Nets
,
by Peter Chini and Roland Meyer.
In Carl Adam Petri: Ideas, Personality, Impact, 2019.
Book | DOI
- Verifying Quantitative Temporal Properties of Procedural Programs,
by Mohammed Faouzi Atig, K Narayan Kumar, Prakash Saivasan, and Ahmed Bouajjani.
In Proceedings of CONCUR 2018.
- BMC with Memory Models as Modules,
by Hernan Ponce-de-Leon, Florian Furbach, Keijo Heljanko, and Roland Meyer.
In Proceedings of FMCAD 2018.
PDF | BibTeX
- Bounded Context Switching for Valence Systems,
by Roland Meyer, Sebastian Muskalla, and Georg Zetzsche.
In Proceedings of CONCUR 2018.
PDF | DOI & BibTex | Full Version @ arXiv | Slides
- Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems,
by Matthew Hague, Roland Meyer, Sebastian Muskalla, and Martin Zimmermann.
In Proceedings of MFCS 2018.
PDF | DOI & BibTex | Full Version @ arXiv | Slides
- Reasoning About Weak Semantics via Strong Semantics,
by Roland Meyer and Sebastian Wolff.
In Principled Software Development - Essays Dedicated to Arnd Poetzsch-Heffter on the
Occasion of his 60th Birthday, 2018.
PDF | Book | DOI
- Fine-Grained Complexity of Safety Verification,
by Peter Chini, Roland Meyer, and Prakash Saivasan.
In Proceedings of TACAS 2018.
Conference Version | DOI/BibTex | Full Version @ arXiv
- Regular Separability of Well-Structured Transition Systems,
by Wojciech Czerwiński, Sławomir Lasota, Roland Meyer, Sebastian Muskalla, K Narayan Kumar, and Prakash Saivasan.
In Proceedings of CONCUR 2018.
PDF | DOI & BibTex | Full Version @ arXiv | Slides | Poster
- Portability Analysis for Axiomatic Memory Models. PORTHOS: One Tool for all Models,
by Roland Meyer, Hernan Ponce-de-Leon, Florian Furbach, and Keijo Heljanko.
In Proceedings of SAS 2017.
DOI | arXiv
- Domains for Higher-Order Games,
by Matthew Hague, Roland Meyer, and Sebastian Muskalla.
In Proceedings of MFCS 2017.
PDF | DOI & BibTex | Full Version @ arXiv | Slides
- Parity games over bounded phase multi-pushdown systems,
by Mohammed Faouzi Atig, K Narayan Kumar, Prakash Saivasan, and Ahmed Bouajjani.
In Proceedings of NETYS 2017.
- Effect Summaries for Thread-Modular Analysis,
by Lukas Holik, Roland Meyer, Tomas Vojnar, and Sebastian Wolff.
In Proceedings of SAS 2017.
PDF | Slides | DOI | arXiv | Code on GitHub
- On the Complexity of Bounded Context Switching,
by Peter Chini, Jonathan Kolberg, Andreas Krebs, Roland Meyer, and Prakash Saivasan.
In Proceedings of ESA 2017.
Conference Version | DOI/BibTex | Full Version @ arXiv
- Locality and Singularity for Store-Atomic Memory Models,
by Egor Derevenetc, Roland Meyer, and Sebastian Schweizer.
In Proceedings of NETYS 2017.
DOI | arXiv
- On the Upward/Downward Closures of Petri Nets,
by Mohamed Faouzi Atig, Roland Meyer, Sebastian Muskalla, and Prakash Saivasan.
In Proceedings of MFCS 2017.
PDF | DOI & BibTex | Full Version @ arXiv | Slides
- Verification of Asynchronous Programs with Nested Locks ,
by Mohammed Faouzi Atig, K Narayan Kumar, Prakash Saivasan, and Ahmed Bouajjani.
In Proceedings of FSTTCS 2017.
- Acceleration in Multi-PushDown Systems,
by Prakash Saivasan, K Narayan Kumar, and Mohammed Faouzi Atig.
In Proceedings of TACAS 2016.
DOI
- On Hierarchical Communication Topologies in the pi-calculus,
by Emanuele D'Osualdo and C.-H. Luke Ong.
In Proceedings of ESOP 2016.
DOI | arXiv | Tool
- Complexity of regular abstractions of one-counter languages,
by Mohammed Faouzi Atig, Dmitry Chistikov, Piotr Hofman, K Narayan Kumar, Prakash Saivasan, and Georg Zetzsche.
In Proceedings of LICS 2016.
arXiv
- Summaries for Context-Free Games,
by Lukas Holik, Roland Meyer, and Sebastian Muskalla.
In Proceedings of FSTTCS 2016.
PDF | DOI & BibTex | Full Version @ arXiv | Slides
- First-order logic with reachability for infinite-state systems,
by Emanuele D'Osualdo, Roland Meyer, and Georg Zetzsche.
In Proceedings of LICS 2016.
PDF | DOI
- Pointer Race Freedom,
by Frederic Haziza, Lukas Holik, Roland Meyer, and Sebastian Wolff.
In Proceedings of VMCAI 2016.
PDF | DOI | BibTeX
- What's Decidable about Availability Languages?,
by Parosh Abdulla, Mohamed Faouzi Atig, Roland Meyer, and Mehdi Seyed Salehi.
In Proceedings of FSTTCS 2015.
PDF | DOI | BibTeX
- Antichains for Recursive Program Verification,
by Lukas Holik and Roland Meyer.
In Proceedings of NETYS 2015.
PDF | Correction | DOI | BibTeX
- Lazy TSO Reachability,
by Ahmed Bouajjani, Georgel Calin, Egor Derevenetc, and Roland Meyer.
In Proceedings of FASE 2015.
arXiv | DOI | BibTeX
- From Program Verification to Time and Space: The Scientific Life of Ernst-Rüdiger Olderog,
by Roland Meyer and Heike Wehrheim.
In Proceedings of Symposium in Honor of Ernst-Rüdiger Olderog.
DOI | BibTeX
- Building A State-Of-The-Art Model Checker,
by Sebastian Wolff.
In 45. Jahrestagung der Gesellschaft für Informatik, Informatik 2015, Informatik, Energie und Umwelt, 28. September - 2.
Oktober 2015 in Cottbus, Deutschland, 2015.
PDF | Slides | Code on GitHub
- The Emptiness Problem for Valence Automata or: Another Decidable Extension of Petri
Nets,
by Georg Zetzsche.
In Proceedings of RP 2015.
DOI
- An Approach to Computing Downward Closures,
by Georg Zetzsche.
In Proceedings of ICALP 2015.
DOI | arXiv
- Computing downward closures for stacked counter automata,
by Georg Zetzsche.
In Proceedings of STACS 2015.
DOI | arXiv
- Bounds on Mobility,
by Reiner Hüchting, Rupak Majumdar, and Roland Meyer.
In Proceedings of CONCUR 2014.
PDF | DOI | BibTeX
- On Boolean closed full trios and rational Kripke frames,
by Markus Lohrey and Georg Zetzsche.
In Proceedings of STACS 2014.
DOI
- Robustness against Power is PSPACE-complete,
by Egor Derevenetc and Roland Meyer.
In Proceedings of ICALP 2014.
arXiv | DOI | BibTeX
- Memory-Model-Aware Testing - a Unified Complexity Analysis,
by Florian Furbach, Roland Meyer, Klaus Schneider, and Maximilian Senftleben.
In Proceedings of ACSD 2014.
ACSD 2014 best paper award.
DOI | PDF
- Checking and Enforcing Robustness against Relaxed Memory Models,
by Ahmed Bouajjani, Egor Derevenetc, and Roland Meyer.
In Proceedings of SE 2014.
PDF
- On Bounded Reachability Analysis of Shared Memory Systems,
by Prakash Saivasan, K Narayan Kumar, Mohammed Faouzi Atig, and Ahmed Bouajjani.
In Proceedings of FSTTCS 2014.
DOI
- The Monoid of Queue Actions,
by Martin Huschenbett, Dietrich Kuske, and Georg Zetzsche.
In Proceedings of MFCS 2014.
DOI | arXiv
- Silent Transitions in Automata with Storage,
by Georg Zetzsche.
In Proceedings of ICALP 2013.
DOI | arXiv
- A Theory of Name Boundedness,
by Reiner Hüchting, Rupak Majumdar, and Roland Meyer.
In Proceedings of CONCUR 2013.
PDF | DOI
- Provenance Verification,
by Rupak Majumdar, Roland Meyer, and Zilong Wang.
In Proceedings of RP 2013.
DOI | BibTeX
- Automatic Verification of Erlang-Style Concurrency,
by Emanuele D'Osualdo, Jonathan Kochems, and C.-H. Luke Ong.
In Proceedings of SAS 13.
DOI | arXiv | Slides | Project's website
- Semilinearity and Context-Freeness of Languages Accepted by Valence Automata,
by P. Buckheister and Georg Zetzsche.
In Proceedings of MFCS 2013.
DOI | arXiv
- Rational Subsets and Submonoids of Wreath Products,
by Markus Lohrey, Benjamin Steinberg, and Georg Zetzsche.
In Proceedings of ICALP 2013.
DOI | arXiv
- A Theory of Partitioned Global Address Spaces,
by Georgel Calin, Egor Derevenetc, Rupak Majumdar, and Roland Meyer.
In Proceedings of FSTTCS 2013.
arXiv | DOI | BibTeX
- Checking and Enforcing Robustness against TSO,
by Ahmed Bouajjani, Egor Derevenetc, and Roland Meyer.
In Proceedings of ESOP 2013.
PDF (full version) | DOI | BibTeX
- Static Provenance Verification for Message Passing Programs,
by Rupak Majumdar, Roland Meyer, and Zilong Wang.
In Proceedings of SAS 2013.
PDF | DOI | BibTeX
- Adjacent Ordered Multi-Pushdown Systems,
by Prakash Saivasan, Mohammed Faouzi Atig, and K Narayan Kumar.
In Proceedings of DLT 13.
DOI
- A Polynomial Translation of Pi-Calculus (FCP) to Safe Petri Nets,
by Roland Meyer, Victor Khomenko, and Reiner Hüchting.
In Proceedings of CONCUR 2012.
PDF | DOI
- Linear-Time Model-Checking for Multithreaded Programs under Scope-Bounding,
by Prakash Saivasan, K Narayan Kumar, Mohammed Faouzi Atig, and Ahmed Bouajjani.
In Proceedings of ATVA 12.
DOI
- Language-Theoretic Abstraction Refinement,
by Zhenyue Long, Georgel Calin, Rupak Majumdar, and Roland Meyer.
In Proceedings of FASE 2012.
ETAPS 2012 best paper award by EAPLS.
DOI | www | BibTeX
- Soter: An Automatic Safety Verifier for Erlang,
by Emanuele D'Osualdo, Jonathan Kochems, and C.-H. Luke Ong.
In Proceedings of AGERE! 12.
DOI | Tool
- An Algorithmic Framework for Coverability in Well-Structured Systems,
by Tim Strazny and Roland Meyer.
In Proceedings of ACSD 2012.
ACSD 2012 best paper award.
DOI | BibTeX
- A Sufficient Condition for Erasing Productions to Be Avoidable,
by Georg Zetzsche.
In Proceedings of DLT 2011.
DOI
- On the Capabilities of Grammars, Automata, and Transducers Controlled by Monoids,
by Georg Zetzsche.
In Proceedings of ICALP 2011.
arXiv | DOI
- Deciding Robustness against Total Store Ordering,
by Ahmed Bouajjani, Roland Meyer, and Eike Möhlmann.
In Proceedings of ICALP 2011.
DOI | BibTeX
- Petri Net Reachability Graphs: Decidability Status of FO Properties,
by Ph. Darondeau, S. Demri, Roland Meyer, and C. Morvan.
In Proceedings of FSTTCS 2011.
DOI | BibTeX
- On Erasing Productions in Random Context Grammars,
by Georg Zetzsche.
In Proceedings of ICALP 2010.
DOI
- Kleene, Rabin, and Scott are available,
by Jochen Hoenicke, Roland Meyer, and Ernst-Rüdiger Olderog.
In Proceedings of CONCUR 2010.
PDF | DOI | BibTeX
- The downward-closure of Petri net languages,
by Peter Habermehl, Roland Meyer, and Harro Wimmel.
In Proceedings of ICALP 2010.
Slides | PDF | DOI | BibTeX
- Petruchio: From dynamic networks to nets,
by Roland Meyer and Tim Strazny.
In Proceedings of CAV 2010.
PDF | DOI | BibTeX
- Checking pi-calculus structural congruence is graph isomorphism complete,
by Victor Khomenko and Roland Meyer.
In Proceedings of ACSD 2009.
DOI | PDF | BibTeX
- Erasing in Petri Net Languages and Matrix Grammars,
by Georg Zetzsche.
In Proceedings of DLT 2009.
DOI
- On the relationship between pi-calculus and finite place/transition Petri nets,
by Roland Meyer and Roberto Gorrieri.
In Proceedings of CONCUR 2009.
Slides | PDF | DOI | BibTeX
- Labeled Step Sequences in Petri Nets,
by Matthias Jantzen and Georg Zetzsche.
In Proceedings of PETRI NETS 2008.
DOI
- A practical approach to verification of mobile systems using net unfoldings,
by Roland Meyer, Victor Khomenko, and Tim Strazny.
In Proceedings of PETRI NETS 2008.
Slides | PDF | DOI | BibTeX
- On boundedness in depth in the pi-calculus,
by Roland Meyer.
In Proceedings of IFIP TCS 2008.
Slides | PDF | DOI | BibTeX
- Model checking data-dependent real-time properties of the European Train Control System,
by Johannes Faber and Roland Meyer.
In Proceedings of FMCAD 2006.
DOI | BibTeX | Slides
- Model checking duration calculus: A practical approach,
by Roland Meyer, Johannes Faber, and Andrey Rybalchenko.
In Proceedings of ICTAC 2006.
PDF | DOI | BibTeX
- Compositional semantics for UML 2.0 sequence diagrams using Petri nets,
by Christoph Eichner, Hans Fleischhack, Roland Meyer, Ulrik Schrimpf, and Christian Stehno.
In Proceedings of SDL 2005.
DOI | BibTeX