Compositional Semantics for UML 2.0 Sequence Diagrams Using Petri Nets. - Christoph Eichner; Hans Fleischhack; Roland Meyer 001; Ulrik Schrimpf; Christian Stehno (SDL Forum, 2005)

Model Checking Data-Dependent Real-Time Properties of the European Train Control System. - Johannes Faber; Roland Meyer 001 (FMCAD, 2006)

Model Checking Duration Calculus: A Practical Approach. - Roland Meyer 001; Johannes Faber; Andrey Rybalchenko (ICTAC, 2006)

Trustworthy software systems: a discussion of basic concepts and terminology. - Steffen Becker 001; Wilhelm Hasselbring; Alexandra Paul; Marko Boskovic; Heiko Koziolek; Jan Ploski; Abhishek Dhama; Henrik Lipskoch; Matthias Rohr; Daniel Winteler; Simon Giesecke; Roland Meyer 001; et al. (ACM SIGSOFT Softw. Eng. Notes, 2006)

On Boundedness in Depth in the pi-Calculus. - Roland Meyer 001 (IFIP TCS, 2008)

Model checking Duration Calculus: a practical approach. - Roland Meyer 001; Johannes Faber; Jochen Hoenicke; Andrey Rybalchenko (Formal Aspects Comput., 2008)

Checking pi-Calculus Structural Congruence is Graph Isomorphism Complete. - Victor Khomenko; Roland Meyer 001 (ACSD, 2009)

On the Relationship between π-Calculus and Finite Place/Transition Petri Nets. - Roland Meyer 001; Roberto Gorrieri (CONCUR, 2009)

Strukturelle Stationarität. - Roland Meyer 001 (Ausgezeichnete Informatikdissertationen, 2009)

A theory of structural stationarity in the pi -Calculus. - Roland Meyer 001 (Acta Informatica, 2009)

A Practical Approach to Verification of Mobile Systems Using Net Unfoldings. - Roland Meyer 001; Victor Khomenko; Tim Strazny (Fundam. Informaticae, 2009)

Structural stationarity in the π-calculus. - Roland Meyer 001 (2009)

Petruchio: From Dynamic Networks to Nets. - Roland Meyer 001; Tim Strazny (CAV, 2010)

Kleene, Rabin, and Scott Are Available. - Jochen Hoenicke; Roland Meyer 001; Ernst-Rüdiger Olderog (CONCUR, 2010)

The Downward-Closure of Petri Net Languages. - Peter Habermehl; Roland Meyer 001; Harro Wimmel (ICALP (2), 2010)

Petri Net Reachability Graphs: Decidability Status of FO Properties. - Philippe Darondeau; Stéphane Demri; Roland Meyer 001; Christophe Morvan (FSTTCS, 2011)

Deciding Robustness against Total Store Ordering. - Ahmed Bouajjani; Roland Meyer 001; Eike Möhlmann (ICALP (2), 2011)

An Algorithmic Framework for Coverability in Well-Structured Systems. - Tim Strazny; Roland Meyer 001 (ACSD, 2012)

A Polynomial Translation of π-Calculus (FCP) to Safe Petri Nets. - Roland Meyer 001; Victor Khomenko; Reiner Hüchting (CONCUR, 2012)

Language-Theoretic Abstraction Refinement. - Zhenyue Long; Georgel Calin; Rupak Majumdar; Roland Meyer 001 (FASE, 2012)

Robustness Checking against TSO: Attacks and Defence - Ahmed Bouajjani; Egor Derevenetc; Roland Meyer 001 (CoRR, 2012)

Petri Net Reachability Graphs: Decidability Status of First Order Properties - Philippe Darondeau; Stéphane Demri; Roland Meyer 001; Christophe Morvan (Log. Methods Comput. Sci., 2012)

A Theory of Name Boundedness. - Reiner Hüchting; Rupak Majumdar; Roland Meyer 001 (CONCUR, 2013)

Checking and Enforcing Robustness against TSO. - Ahmed Bouajjani; Egor Derevenetc; Roland Meyer 001 (ESOP, 2013)

A Theory of Partitioned Global Address Spaces. - Georgel Calin; Egor Derevenetc; Rupak Majumdar; Roland Meyer 001 (FSTTCS, 2013)

Provenance Verification. - Rupak Majumdar; Roland Meyer 001; Zilong Wang 004 (RP, 2013)

Static Provenance Verification for Message Passing Programs. - Rupak Majumdar; Roland Meyer 001; Zilong Wang 004 (SAS, 2013)

A Polynomial Translation of pi-calculus FCPs to Safe Petri Nets. - Victor Khomenko; Roland Meyer 001; Reiner Hüchting (Log. Methods Comput. Sci., 2013)

Bounds on Mobility. - Reiner Hüchting; Rupak Majumdar; Roland Meyer 001 (CONCUR, 2014)

Robustness against Power is PSpace-complete. - Egor Derevenetc; Roland Meyer 001 (ICALP (2), 2014)

Robustness against Relaxed Memory Models. - Ahmed Bouajjani; Egor Derevenetc; Roland Meyer 001 (Software Engineering, 2014)

From Program Verification to Time and Space: The Scientific Life of Ernst-Rüdiger Olderog. - Roland Meyer 001; Heike Wehrheim (Correct System Design, 2015)

Lazy TSO Reachability. - Ahmed Bouajjani; Georgel Calin; Egor Derevenetc; Roland Meyer 001 (FASE, 2015)

What's Decidable about Availability Languages?. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Roland Meyer 001; Mehdi Seyed Salehi (FSTTCS, 2015)

Antichains for the Verification of Recursive Programs. - Lukás Holík; Roland Meyer 001 (NETYS, 2015)

Memory-Model-Aware Testing: A Unified Complexity Analysis. - Florian Furbach; Roland Meyer 001; Klaus Schneider 001; Maximilian Senftleben (ACM Trans. Embed. Comput. Syst., 2015)

Summaries for Context-Free Games. - Lukás Holík; Roland Meyer 001; Sebastian Muskalla (FSTTCS, 2016)

First-order logic with reachability for infinite-state systems. - Emanuele D'Osualdo; Roland Meyer 001; Georg Zetzsche (LICS, 2016)

Pointer Race Freedom. - Frédéric Haziza; Lukás Holík; Roland Meyer 001; Sebastian Wolff 001 (VMCAI, 2016)

On the Complexity of Bounded Context Switching. - Peter Chini; Jonathan Kolberg; Roland Meyer 001; Prakash Saivasan (CoRR, 2016)

Antichains for Inclusion Games. - Lukás Holík; Roland Meyer 001; Sebastian Muskalla (CoRR, 2016)

Munchausen Iteration. - Roland Meyer 001; Sebastian Muskalla (CoRR, 2016)

On the Complexity of Bounded Context Switching. - Peter Chini; Jonathan Kolberg; Andreas Krebs; Roland Meyer 001; Prakash Saivasan (ESA, 2017)

On the Upward/Downward Closures of Petri Nets. - Mohamed Faouzi Atig; Roland Meyer 001; Sebastian Muskalla; Prakash Saivasan (MFCS, 2017)

Domains for Higher-Order Games. - Matthew Hague; Roland Meyer 001; Sebastian Muskalla (MFCS, 2017)

Locality and Singularity for Store-Atomic Memory Models. - Egor Derevenetc; Roland Meyer 001; Sebastian Schweizer (NETYS, 2017)

Effect Summaries for Thread-Modular Analysis - Sound Analysis Despite an Unsound Heuristic. - Lukás Holík; Roland Meyer 001; Tomás Vojnar; Sebastian Wolff 001 (SAS, 2017)

Portability Analysis for Weak Memory Models. PORTHOS: One Tool for all Models. - Hernán Ponce de León; Florian Furbach; Keijo Heljanko; Roland Meyer 001 (SAS, 2017)

Effect Summaries for Thread-Modular Analysis. - Lukás Holík; Roland Meyer 001; Tomás Vojnar; Sebastian Wolff 001 (CoRR, 2017)

Portability Analysis for Axiomatic Memory Models. PORTHOS: One Tool for all Models. - Hernán Ponce de León; Florian Furbach; Keijo Heljanko; Roland Meyer 001 (CoRR, 2017)

Liveness Verification and Synthesis: New Algorithms for Recursive Programs. - Roland Meyer 001; Sebastian Muskalla; Elisabeth Neumann (CoRR, 2017)

Message from the Guest Editors. - Stefan Haar; Roland Meyer 001 (ACM Trans. Embed. Comput. Syst., 2017)

Reasoning About Weak Semantics via Strong Semantics. - Roland Meyer 001; Sebastian Wolff 001 (Principled Software Development, 2018)

Regular Separability of Well-Structured Transition Systems. - Wojciech Czerwinski; Slawomir Lasota 001; Roland Meyer 001; Sebastian Muskalla; K. Narayan Kumar; Prakash Saivasan (CONCUR, 2018)

Bounded Context Switching for Valence Systems. - Roland Meyer 001; Sebastian Muskalla; Georg Zetzsche (CONCUR, 2018)

BMC with Memory Models as Modules. - Hernán Ponce de León; Florian Furbach; Keijo Heljanko; Roland Meyer 001 (FMCAD, 2018)

Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems. - Matthew Hague; Roland Meyer 001; Sebastian Muskalla; Martin Zimmermann 002 (MFCS, 2018)

Fast Witness Counting. - Peter Chini; Rehab Massoud; Roland Meyer 001; Prakash Saivasan (CoRR, 2018)

Inductive Counting and the Reachability Problem for Petri Nets. - Peter Chini; Roland Meyer 001 (Carl Adam Petri: Ideas, Personality, Impact, 2019)

BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings. - Natalia Gavrilenko; Hernán Ponce de León; Florian Furbach; Keijo Heljanko; Roland Meyer 001 (CAV (1), 2019)

Temporal Tracing of On-Chip Signals using Timeprints. - Rehab Massoud; Hoang M. Le; Peter Chini; Prakash Saivasan; Roland Meyer 001; Rolf Drechsler (DAC, 2019)

Complexity of Liveness in Parameterized Systems. - Peter Chini; Roland Meyer 001; Prakash Saivasan (FSTTCS, 2019)

Sicherheit, Zuverlässigkeit, Korrektheit. - Juliane Krämer; Roland Meyer 001 (GI-Jahrestagung, 2019)

Decoupling lock-free data structures from memory reclamation for static analysis. - Roland Meyer 001; Sebastian Wolff 001 (Proc. ACM Program. Lang., 2019)

On the Complexity of Multi-Pushdown Games. - Roland Meyer 001; Sören van der Wall (FSTTCS, 2020)

On the State Reachability Problem for Concurrent Programs Under Power. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Ahmed Bouajjani; Egor Derevenetc; Carl Leonardsson; Roland Meyer 001 (NETYS, 2020)

Dartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution). - Hernán Ponce de León; Florian Furbach; Keijo Heljanko; Roland Meyer 001 (TACAS (2), 2020)

Fine-Grained Complexity of Safety Verification. - Peter Chini; Roland Meyer 001; Prakash Saivasan (J. Autom. Reason., 2020)

Pointer life cycle types for lock-free data structures with memory reclamation. - Roland Meyer 001; Sebastian Wolff 001 (Proc. ACM Program. Lang., 2020)

Dartagnan: Leveraging Compiler Optimizations and the Price of Precision (Competition Contribution). - Hernán Ponce de León; Thomas Haas; Roland Meyer 001 (TACAS (2), 2021)

Safety Verification of Parameterized Systems under Release-Acquire. - Adwait Godbole; Shankara Narayanan Krishna; Roland Meyer 001 (CoRR, 2021)

Verifying and Optimizing Compact NUMA-Aware Locks on Weak Memory Models. - Antonio Paolillo; Hernán Ponce de León; Thomas Haas; Diogo Behrens; Rafael Lourenco de Lima Chehab; Ming Fu; Roland Meyer 001 (CoRR, 2021)

Model-Based Fault Classification for Automotive Software. - Mike Becker; Roland Meyer 001; Tobias Runge; Ina Schaefer; Sören van der Wall; Sebastian Wolff 001 (APLAS, 2022)

Parameterized Verification under Release Acquire is PSPACE-complete. - Shankaranarayanan Krishna; Adwait Godbole; Roland Meyer 001; Soham Chakraborty 001 (PODC, 2022)

Dartagnan: SMT-based Violation Witness Validation (Competition Contribution). - Hernán Ponce de León; Thomas Haas; Roland Meyer 001 (TACAS (2), 2022)

Liveness in broadcast networks. - Peter Chini; Roland Meyer 001; Prakash Saivasan (Computing, 2022)

CAAT: consistency as a theory. - Thomas Haas; Roland Meyer 001; Hernán Ponce de León (Proc. ACM Program. Lang., 2022)

A concurrent program logic with a future and history. - Roland Meyer 001; Thomas Wies; Sebastian Wolff 001 (Proc. ACM Program. Lang., 2022)

nekton: A Linearizability Proof Checker. - Roland Meyer 001; Anton Opaterny; Thomas Wies; Sebastian Wolff 001 (CAV (1), 2023)

Separability and Non-Determinizability of WSTS. - Eren Keskin; Roland Meyer 001 (CONCUR, 2023)

Regular Separability in Büchi VASS. - Pascal Baumann 001; Roland Meyer 001; Georg Zetzsche (STACS, 2023)

Make Flows Small Again: Revisiting the Flow Framework. - Roland Meyer 001; Thomas Wies; Sebastian Wolff 001 (TACAS (1), 2023)

Contextual Equivalence for Alternation and Urgency. - Eren Keskin; Roland Meyer 001; Sören van der Wall (CoRR, 2023)

Context-Aware Separation Logic. - Roland Meyer 001; Thomas Wies; Sebastian Wolff 001 (CoRR, 2023)

Embedding Hindsight Reasoning in Separation Logic. - Roland Meyer 001; Thomas Wies; Sebastian Wolff 001 (Proc. ACM Program. Lang., 2023)

Static Analysis of Memory Models for SMT Encodings. - Thomas Haas; René Pascasl Maseli; Roland Meyer 001; Hernán Ponce de León (Proc. ACM Program. Lang., 2023)

Urgency Annotations for Alternating Choices. - Eren Keskin; Roland Meyer 001; Sören van der Wall (Principles of Verification (3), 2024)

Separability in Büchi VASS and Singly Non-Linear Systems of Inequalities. - Pascal Baumann 001; Eren Keskin; Roland Meyer 001; Georg Zetzsche (ICALP, 2024)

On the Separability Problem of VASS Reachability Languages. - Eren Keskin; Roland Meyer 001 (LICS, 2024)

Realizability in Semantics-Guided Synthesis Done Eagerly. - Roland Meyer 001; Jakob Tepe; Sebastian Wolff 001 (CoRR, 2024)

I still know it's you! On Challenges in Anonymizing Source Code. - Micha Horlboge; Erwin Quiring; Roland Meyer 001; Konrad Rieck (Proc. Priv. Enhancing Technol., 2024)

SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations. - Sören van der Wall; Roland Meyer 001 (Proc. ACM Program. Lang., 2025)

PVASS Reachability is Decidable. - Roland Guttenberg; Eren Keskin; Roland Meyer 001 (CoRR, 2025)