## Publications

### Recent

- Temporal Tracing of On-chip Signals using Timeprints,
by , , , , , and .

DAC 2019 - BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings,
by Natalia Gavrilenko, Hernan Ponce-de-Leon, , Keijo Heljanko, and .

CAV 2019 - Liveness Verification and Synthesis: New Algorithms for Recursive Programs,
by , , and .

arXiv - Fast Witness Counting,
by , , , and .

arXiv - Munchausen Iteration,
by and .

arXiv

### Conference contributions

- Decoupling Lock-Free Data Structures from Memory Reclamation for Static Analysis,
by and .

In Proceedings of POPL 2019. Artifact evaluated: functional&reusable.

PDF | Slides | Project Page | DOI | arXiv - Verifying Quantitative Temporal Properties of Procedural Programs,
by , K Narayan Kumar, , and .

In Proceedings of CONCUR 2018.

- BMC with Memory Models as Modules,
by Hernan Ponce-de-Leon, , Keijo Heljanko, and .

In Proceedings of FMCAD 2018.

PDF | BibTeX - Bounded Context Switching for Valence Systems,
by , , and .

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, , , and Martin Zimmermann.

In Proceedings of MFCS 2018.

PDF | DOI & BibTex | Full Version @ arXiv | Slides - Reasoning About Weak Semantics via Strong Semantics,
by and .

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

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, , , K Narayan Kumar, and .

In Proceedings of CONCUR 2018.

PDF | DOI & BibTex | Full Version @ arXiv | Slides | Poster -
Inductive Counting and the Reachability Problem for Petri Nets
,
by and .

In Carl Adam Petri: Ideas, Personality, Impact, 2018.

Book - Portability Analysis for Axiomatic Memory Models. PORTHOS: One Tool for all Models,
by , Hernan Ponce-de-Leon, , and Keijo Heljanko.

In Proceedings of SAS 2017.

DOI | arXiv - Domains for Higher-Order Games,
by Matthew Hague, , and .

In Proceedings of MFCS 2017.

PDF | DOI & BibTex | Full Version @ arXiv | Slides - Parity games over bounded phase multi-pushdown systems,
by , K Narayan Kumar, , and .

In Proceedings of NETYS 2017.

- Effect Summaries for Thread-Modular Analysis,
by , , , and .

In Proceedings of SAS 2017.

PDF | Slides | DOI | arXiv | Code on GitHub - On the Complexity of Bounded Context Switching,
by , , , , and .

In Proceedings of ESA 2017.

Conference Version | DOI/BibTex | Full Version @ arXiv - Locality and Singularity for Store-Atomic Memory Models,
by , , and .

In Proceedings of NETYS 2017.

DOI | arXiv - On the Upward/Downward Closures of Petri Nets,
by Mohamed Faouzi Atig, , , and .

In Proceedings of MFCS 2017.

PDF | DOI & BibTex | Full Version @ arXiv | Slides - Verification of Asynchronous Programs with Nested Locks ,
by , K Narayan Kumar, , and .

In Proceedings of FSTTCS 2017.

- Acceleration in Multi-PushDown Systems,
by , K Narayan Kumar, and .

In Proceedings of TACAS 2016.

DOI - Complexity of regular abstractions of one-counter languages,
by , , , K Narayan Kumar, , and .

In Proceedings of LICS 2016.

arXiv - On Hierarchical Communication Topologies in the pi-calculus,
by and .

In Proceedings of ESOP 2016.

DOI | arXiv | Tool - Summaries for Context-Free Games,
by , , and .

In Proceedings of FSTTCS 2016.

PDF | DOI & BibTex | Full Version @ arXiv | Slides - First-order logic with reachability for infinite-state systems,
by , , and .

In Proceedings of LICS 2016.

PDF | DOI - Pointer Race Freedom,
by Frederic Haziza, , , and .

In Proceedings of VMCAI 2016.

PDF | DOI | BibTeX - What's Decidable about Availability Languages?,
by Parosh Abdulla, Mohamed Faouzi Atig, , and Mehdi Seyed Salehi.

In Proceedings of FSTTCS 2015.

PDF | DOI | BibTeX - Antichains for Recursive Program Verification,
by and .

In Proceedings of NETYS 2015.

PDF | DOI | BibTeX - Lazy TSO Reachability,
by Ahmed Bouajjani, , , and .

In Proceedings of FASE 2015.

arXiv | DOI | BibTeX - From Program Verification to Time and Space: The Scientific Life of Ernst-Rüdiger Olderog,
by 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 .

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 .

In Proceedings of RP 2015.

DOI - An Approach to Computing Downward Closures,
by .

In Proceedings of ICALP 2015.

DOI | arXiv - Computing downward closures for stacked counter automata,
by .

In Proceedings of STACS 2015.

DOI | arXiv - Bounds on Mobility,
by , Rupak Majumdar, and .

In Proceedings of CONCUR 2014.

PDF | DOI | BibTeX - On Boolean closed full trios and rational Kripke frames,
by and .

In Proceedings of STACS 2014.

DOI - Robustness against Power is PSPACE-complete,
by and .

In Proceedings of ICALP 2014.

arXiv | DOI | BibTeX - Memory-Model-Aware Testing - a Unified Complexity Analysis,
by , , , and .

In Proceedings of ACSD 2014.*ACSD 2014 best paper award.*

DOI | PDF - Checking and Enforcing Robustness against Relaxed Memory Models,
by Ahmed Bouajjani, , and .

In Proceedings of SE 2014.

PDF - On Bounded Reachability Analysis of Shared Memory Systems,
by , K Narayan Kumar, , and .

In Proceedings of FSTTCS 2014.

DOI - The Monoid of Queue Actions,
by , , and .

In Proceedings of MFCS 2014.

DOI | arXiv - Silent Transitions in Automata with Storage,
by .

In Proceedings of ICALP 2013.

DOI | arXiv - A Theory of Name Boundedness,
by , Rupak Majumdar, and .

In Proceedings of CONCUR 2013.

PDF | DOI - Provenance Verification,
by Rupak Majumdar, , and Zilong Wang.

In Proceedings of RP 2013.

DOI | BibTeX - Automatic Verification of Erlang-Style Concurrency,
by , Jonathan Kochems, and .

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 .

In Proceedings of MFCS 2013.

DOI | arXiv - Rational Subsets and Submonoids of Wreath Products,
by , , and .

In Proceedings of ICALP 2013.

DOI | arXiv - A Theory of Partitioned Global Address Spaces,
by , , Rupak Majumdar, and .

In Proceedings of FSTTCS 2013.

arXiv | DOI | BibTeX - Checking and Enforcing Robustness against TSO,
by Ahmed Bouajjani, , and .

In Proceedings of ESOP 2013.

PDF (full version) | DOI | BibTeX - Static Provenance Verification for Message Passing Programs,
by Rupak Majumdar, , and Zilong Wang.

In Proceedings of SAS 2013.

PDF | DOI | BibTeX - Adjacent Ordered Multi-Pushdown Systems,
by , , and K Narayan Kumar.

In Proceedings of DLT 13.

DOI - Linear-Time Model-Checking for Multithreaded Programs under Scope-Bounding,
by , K Narayan Kumar, , and .

In Proceedings of ATVA 12.

DOI - A Polynomial Translation of Pi-Calculus (FCP) to Safe Petri Nets,
by , Victor Khomenko, and .

In Proceedings of CONCUR 2012.

PDF | DOI - Language-Theoretic Abstraction Refinement,
by Zhenyue Long, , Rupak Majumdar, and .

In Proceedings of FASE 2012.*ETAPS 2012 best paper award by EAPLS.*

DOI | www | BibTeX - Soter: An Automatic Safety Verifier for Erlang,
by , Jonathan Kochems, and .

In Proceedings of AGERE! 12.

DOI | Tool - An Algorithmic Framework for Coverability in Well-Structured Systems,
by Tim Strazny and .

In Proceedings of ACSD 2012.*ACSD 2012 best paper award.*

DOI | BibTeX - A Sufficient Condition for Erasing Productions to Be Avoidable,
by .

In Proceedings of DLT 2011.

DOI - On the Capabilities of Grammars, Automata, and Transducers Controlled by Monoids,
by .

In Proceedings of ICALP 2011.

arXiv | DOI - Deciding Robustness against Total Store Ordering,
by Ahmed Bouajjani, , 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, , and C. Morvan.

In Proceedings of FSTTCS 2011.

DOI | BibTeX - On Erasing Productions in Random Context Grammars,
by .

In Proceedings of ICALP 2010.

DOI - Kleene, Rabin, and Scott are available,
by Jochen Hoenicke, , and Ernst-Rüdiger Olderog.

In Proceedings of CONCUR 2010.

PDF | DOI | BibTeX - The downward-closure of Petri net languages,
by Peter Habermehl, , and Harro Wimmel.

In Proceedings of ICALP 2010.

Slides | PDF | DOI | BibTeX - Petruchio: From dynamic networks to nets,
by and Tim Strazny.

In Proceedings of CAV 2010.

PDF | DOI | BibTeX - Checking pi-calculus structural congruence is graph isomorphism complete,
by Victor Khomenko and .

In Proceedings of ACSD 2009.

DOI | PDF | BibTeX - Erasing in Petri Net Languages and Matrix Grammars,
by .

In Proceedings of DLT 2009.

DOI - On the relationship between pi-calculus and finite place/transition Petri nets,
by and Roberto Gorrieri.

In Proceedings of CONCUR 2009.

Slides | PDF | DOI | BibTeX - Labeled Step Sequences in Petri Nets,
by and .

In Proceedings of PETRI NETS 2008.

DOI - A practical approach to verification of mobile systems using net unfoldings,
by , Victor Khomenko, and Tim Strazny.

In Proceedings of PETRI NETS 2008.

Slides | PDF | DOI | BibTeX - On boundedness in depth in the pi-calculus,
by .

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 .

In Proceedings of FMCAD 2006.

DOI | BibTeX | Slides - Model checking duration calculus: A practical approach,
by , 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, , Ulrik Schrimpf, and Christian Stehno.

In Proceedings of SDL 2005.

DOI | BibTeX

### Editor

- Stefan Haar and Special Issue on ACSD 2015, ACM Transactions on Embedded Computing Systems (TECS),
16(2).
ACM, 2017.

Webpage | BibTeX
, editors.
- Proceedings of the 28th International Conference on Concurrency Theory (CONCUR),
Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017.

Webpage | BibTeX
and Uwe Nestmann, editors.
- Stefan Haar and Proceedings of the 15th International Conference on Application of Concurrency to
System Design (ACSD),
IEEE Computer Society Press, 2015.

Webpage | BibTeX
, 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
, Andre Platzer, and Heike Wehrheim, editors.
- M. Diehl, H. Lipskoch, Proceedings des gemeinsamen
Workshops der Graduiertenkollegs
,
4 of Trustworthy Software Systems.
GITO, 2008.

, and C. Storm, editors.

### Journal articles

- Knapsack and subset sum problems in nilpotent, polycyclic, and co-context-free groups,
by , , and .

Contemporary Mathematics, 2016.

arXiv - Rational subsets and submonoids of wreath products,
by , , and .

Information and Computation, 2015.

DOI | arXiv - Memory-Model-Aware Testing - a Unified Complexity Analysis,
by , , , and .

ACM Transactions on Embedded Computing Systems (TECS), 2015.

PDF | BibTeX - A Polynomial Translation of Pi-Calculus (FCP) to Safe Petri Nets,
by Victor Khomenko, , and .

Logical Methods in Computer Science, 2013.

arXiv | BibTeX - Petri Net Reachability Graphs: Decidability Status of FO Properties,
by Ph. Darondeau, S. Demri, , and C. Morvan.

Logical Methods in Computer Science, 2012.

BibTeX - Toward Understanding the Generative Capacity of Erasing Rules in Matrix Grammars,
by .

International Journal of Foundations of Computer Science, 2011.

DOI - A Theory of Structural Stationarity in the Pi-Calculus,
by .

Acta Informatica, 2009.

DOI | BibTeX - CoLoSS: The Coalgebraic Logic Satisfiability Solver,
by , Robert S. R. Myers, Dirk Pattinson, and Lutz Schröder.

Electr. Notes Theor. Comput. Sci., 2009.

DOI - Multiset Pushdown Automata,
by , , and .

Fundamenta Informaticae, 2009.

DOI - Properties of Multiset Language Classes Defined by Multiset Pushdown Automata,
by , , and .

Fundamenta Informaticae, 2009.

DOI - Structural analysis in the problem of decompilation,
by and K.N. Dolgova.

Collection of Young Scientists' Articles, 2009.

- A Practical Approach to Verification of Mobile Systems using Net Unfoldings,
by , Victor Khomenko, and Tim Strazny.

Fundamenta Informaticae, 2009.

DOI | BibTeX - Structural analysis in the problem of decompilation,
by and K.N. Dolgova.

Applied Informatics, 2009.

PDF | BibTeX - Petri Net Controlled Finite Automata,
by , , , , and .

Fundamenta Informaticae, 2008.

- Model Checking Duration Calculus: A Practical Approach.,
by , Johannes Faber, Jochen Hoenicke, and Andrey Rybalchenko.

Formal Aspects of Computing, 2008.

PDF | DOI | BibTeX - Language Classes Defined by Concurrent Finite Automata,
by , , and .

Fundamenta Informaticae, 2008.

- Methods and algorithms for reconstructing assembler programs into high level language,
by K.N. Dolgova, A. Chernov, and .

Problems of Information Security, 2008.

PDF | BibTeX - Trustworthy Software Systems: A Discussion of Basic Concepts and Terminology.,
by 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

- Thread Summaries for Lock-Free Data Structures,
by .

In Proceedings of the 28th Nordic Workshop on Programming Theory (NWPT'16), 2016.

PDF | Slides | Code on GitHub | Proceedings - SmartDec: Approaching C++ Decompilation,
by A. Fokin, , A. Chernov, and K. Troshina.

In Proceedings of 18th Working Conference on Reverse Engineering. Limerick, Ireland, 2011.

IEEE | DOI | BibTeX - Reconstruction of Composite Types for Decompilation,
by K. Troshina, , and A. Chernov.

In Proceedings of 10th IEEE International Working Conference on Source Code Analysis and Manipulation. Timisoara, Romania, 2010.

IEEE | DOI | BibTeX - Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains,
by , Pepijn Crouzen, Pedro R. D'Argenio, Ernst Moritz Hahn, and Lijun Zhang.

In Model Checking Software - 17th International SPIN Workshop, Enschede, The Netherlands, September 27-29, 2010. Proceedings, 2010.

DOI - Concurrent finite automata and related language classes (an overview),
by and .

In Automata, Formal Languages and Algebraic Systems, Proceedings of AFLAS 2008, 2010.

DOI - Strukturelle Stationarität,
by .

In Ausgezeichnete Informatik Dissertationen, 2009.

PDF, in German | BibTeX - Automata-theoretic verification based on counterexample specifications,
by Ernst-Rüdiger Olderog and .

In Informatik als Dialog zwischen Theorie und Anwendung, 2009.

DOI | BibTeX - C Decompilation: Is It Possible?,
by K. Troshina, A. Chernov, and .

In Proceedings of International Workshop on Program Understanding. Altai Mountains, Russia, 2009.

PDF | BibTeX - Properties of Multiset Language Classes Defined by Multiset Storage Automata,
by , , and .

In Proceedings of the Workshop CS&P'2008, 2008.

- Multiset Storage Automata,
by , , and .

In Proceedings of the Workshop CS&P'2008, 2008.

- On Concurrent Finite Automata,
by , , , , and .

In Proceedings of the Workshop CS&P'2007, 2007.

- A Petri net semantics for pi-calculus verification,
by .

In Dagstuhl "zehn plus eins", 2007.

BibTeX - On Languages Accepted by Concurrent Finite Automata,
by , , and .

In Proceedings of the Workshop CS&P'2007, 2007.

- Finite Automata Controlled by Petri Nets,
by , , and .

In Proceedings of the 14th Workshop; Algorithmen und Werkzeuge für Petrinetze, 2007.

- Model checking the pi-calculus,
by .

In Proc. of the International Research Training Groups Workshop, 2006.

BibTeX

### Theses

- Runtime Verification of Sequential Consistency for ARM,
Master's Thesis by .

TU Braunschweig, 2017.

- Algorithms for Context-free Games: A Comparison of Saturation, Guess&Check and Summarization,
Master's Thesis by .

Technische Universität Kaiserslautern, 2017.

PDF - Lifetime Analysis for Whiley,
Master's Thesis by .

Technische Universität Kaiserslautern, 2016.

PDF | Slides | More on Whiley | Code Contribution - Monoids as Storage Mechanisms,
PhD thesis by .

Technische Universität Kaiserslautern, 2016.

PDF - Verification Techniques for TSO-Relaxed Programs,
PhD Thesis by .

Technische Universität Kaiserslautern, 2016.

PDF - Analysis of Automata-theoretic models of Concurrent Recursive Programs,
PhD Thesis by .

Chennai Mathematical Institute, 2016.

PDF - Computing the Deligne number of curve singularities and an algorithmic framework for
differential algebras in Singular,
Master Thesis by .

Technische Universität Kaiserslautern, 2015.

PDF - Computing boundaries of tropical varieties,
Master Thesis by .

Technische Universität Kaiserslautern, 2015.

PDF - Thread-Modular Reasoning for Heap-Manipulating Programs: Exploiting Pointer Race Freedom,
Master's Thesis by .

Technische Universität Kaiserslautern, 2015.

PDF | Slides | Code on GitHub - Verification of Message Passing Concurrent Systems,
PhD Thesis by .

University of Oxford, 2015.

PDF - Robustness against Relaxed Memory Models,
PhD thesis by .

University of Kaiserslautern, 2015.

PDF | BibTeX - Automata-Theoretic Control for Total Store Ordering Architectures,
Master Thesis by .

Technische Universität Kaiserslautern, 2012.

PDF - Scheduler-Quantified Time-Bounded Reachability for Distributed Input/Output Interactive
Probabilistic Chains,
MSc Thesis by .

Saarland University, 2010.

PDF - On Erasing Productions in Grammars with Regulated Rewriting,
Diplomarbeit by .

Universität Hamburg, 2010.

- Reconstruction of C++ control flow structures from a low-level program,
Diploma Thesis by .

Moscow State University, 2010.

- Structural Stationarity in the pi-Calculus,
PhD thesis by .

Department of Computing Science, University of Oldenburg, 2009.

Slides | PDF | BibTeX - Model-Checking von Phasen-Event-Automaten bezüglich Duration Calculus Formeln mittels Testautomaten,
Master's thesis by .

Department of Computing Science, University of Oldenburg, 2005.

PDF, in German | BibTeX

### Technical Reports

- A Polynomial Translation of Pi-Calculus (FCP) to Safe Petri Nets,
by , Victor Khomenko, and .

Technical Report CS-TR-1323, School of Computing Science, Newcastle University, 2012.

PDF - Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains,
by , Pepijn Crouzen, Pedro R. D'Argenio, Ernst Moritz Hahn, and Lijun Zhang.

Technical Report 64, Sonderforschungsbereiche (SFB)/Transregio (TR) 14 AVACS, 2010.

PDF - A Note on Hack's Conjecture, Parikh Images of Matrix Languages and Multiset Grammars,
by .

Technical Report FBI-HH-B-289/09, University of Hamburg, Department of Computer Science, 2009.

OPUS - Automated Checking of Observational Equivalence for an Extended Spi Calculus,
by , Markus Rabe, and Raphael Reischuk.

Technical Report , Student Seminar at Saarland University, 2009.

PDF - Checking pi-calculus structural congruence is graph isomorphism complete,
by Victor Khomenko and .

Technical Report CS-TR-1100, School of Computing Science, Newcastle University, 2008.

PDF | BibTeX - On depth and breadth in the pi-calculus,
by .

Technical Report 01/08, Department of Computing Science, University of Oldenburg, 2008.

BibTeX - A practical approach to verification of mobile systems using net unfoldings,
by , Victor Khomenko, and Tim Strazny.

Technical Report CS-TR-1064, School of Computing Science, Newcastle University, 2008.

PDF | BibTeX