Theoretical Computer Science

Conference contributions

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

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

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

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

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

77. A Framework for Consistency Algorithms, by Peter Chini and Prakash Saivasan.
    In Proceedings of FSTTCS 2020.
    Conference Version | DOI/BibTex | Full Version @ arXiv

76. On the Complexity of Multi-Pushdown Games, by Roland Meyer and Sören van der Wall.
    In Proceedings of FSTTCS 2020.
    DOI | PDF

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

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

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

72. Sicherheit, Zuverlässigkeit, Korrektheit, by Juliane Krämer and Roland Meyer.
    In Proceedings of INFORMATIK 2019.
    DOI | BibTeX

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

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

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

68. Verifying Quantitative Temporal Properties of Procedural Programs, by Mohammed Faouzi Atig, K Narayan Kumar, Prakash Saivasan, and Ahmed Bouajjani.
    In Proceedings of CONCUR 2018.
    

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

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

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

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

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

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

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

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

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

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

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

56. Locality and Singularity for Store-Atomic Memory Models, by Egor Derevenetc, Roland Meyer, and Sebastian Schweizer.
    In Proceedings of NETYS 2017.
    DOI | arXiv

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

54. Verification of Asynchronous Programs with Nested Locks , by Mohammed Faouzi Atig, K Narayan Kumar, Prakash Saivasan, and Ahmed Bouajjani.
    In Proceedings of FSTTCS 2017.
    

53. Acceleration in Multi-PushDown Systems, by Prakash Saivasan, K Narayan Kumar, and Mohammed Faouzi Atig.
    In Proceedings of TACAS 2016.
    DOI

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

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

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

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

48. Pointer Race Freedom, by Frederic Haziza, Lukas Holik, Roland Meyer, and Sebastian Wolff.
    In Proceedings of VMCAI 2016.
    PDF | DOI | BibTeX

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

46. Antichains for Recursive Program Verification, by Lukas Holik and Roland Meyer.
    In Proceedings of NETYS 2015.
    PDF | Correction | DOI | BibTeX

45. Lazy TSO Reachability, by Ahmed Bouajjani, Georgel Calin, Egor Derevenetc, and Roland Meyer.
    In Proceedings of FASE 2015.
    arXiv | DOI | BibTeX

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

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

42. The Emptiness Problem for Valence Automata or: Another Decidable Extension of Petri Nets, by Georg Zetzsche.
    In Proceedings of RP 2015.
    DOI

41. An Approach to Computing Downward Closures, by Georg Zetzsche.
    In Proceedings of ICALP 2015.
    DOI | arXiv

40. Computing downward closures for stacked counter automata, by Georg Zetzsche.
    In Proceedings of STACS 2015.
    DOI | arXiv

39. Bounds on Mobility, by Reiner Hüchting, Rupak Majumdar, and Roland Meyer.
    In Proceedings of CONCUR 2014.
    PDF | DOI | BibTeX

38. On Boolean closed full trios and rational Kripke frames, by Markus Lohrey and Georg Zetzsche.
    In Proceedings of STACS 2014.
    DOI

37. Robustness against Power is PSPACE-complete, by Egor Derevenetc and Roland Meyer.
    In Proceedings of ICALP 2014.
    arXiv | DOI | BibTeX

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

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

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

33. The Monoid of Queue Actions, by Martin Huschenbett, Dietrich Kuske, and Georg Zetzsche.
    In Proceedings of MFCS 2014.
    DOI | arXiv

32. Silent Transitions in Automata with Storage, by Georg Zetzsche.
    In Proceedings of ICALP 2013.
    DOI | arXiv

31. A Theory of Name Boundedness, by Reiner Hüchting, Rupak Majumdar, and Roland Meyer.
    In Proceedings of CONCUR 2013.
    PDF | DOI

30. Provenance Verification, by Rupak Majumdar, Roland Meyer, and Zilong Wang.
    In Proceedings of RP 2013.
    DOI | BibTeX

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

28. Semilinearity and Context-Freeness of Languages Accepted by Valence Automata, by P. Buckheister and Georg Zetzsche.
    In Proceedings of MFCS 2013.
    DOI | arXiv

27. Rational Subsets and Submonoids of Wreath Products, by Markus Lohrey, Benjamin Steinberg, and Georg Zetzsche.
    In Proceedings of ICALP 2013.
    DOI | arXiv

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

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

24. Static Provenance Verification for Message Passing Programs, by Rupak Majumdar, Roland Meyer, and Zilong Wang.
    In Proceedings of SAS 2013.
    PDF | DOI | BibTeX

23. Adjacent Ordered Multi-Pushdown Systems, by Prakash Saivasan, Mohammed Faouzi Atig, and K Narayan Kumar.
    In Proceedings of DLT 13.
    DOI

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

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

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

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

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

17. A Sufficient Condition for Erasing Productions to Be Avoidable, by Georg Zetzsche.
    In Proceedings of DLT 2011.
    DOI

16. On the Capabilities of Grammars, Automata, and Transducers Controlled by Monoids, by Georg Zetzsche.
    In Proceedings of ICALP 2011.
    arXiv | DOI

15. Deciding Robustness against Total Store Ordering, by Ahmed Bouajjani, Roland Meyer, and Eike Möhlmann.
    In Proceedings of ICALP 2011.
    DOI | BibTeX

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

13. On Erasing Productions in Random Context Grammars, by Georg Zetzsche.
    In Proceedings of ICALP 2010.
    DOI

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

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

10. Petruchio: From dynamic networks to nets, by Roland Meyer and Tim Strazny.
    In Proceedings of CAV 2010.
    PDF | DOI | BibTeX

9. Checking pi-calculus structural congruence is graph isomorphism complete, by Victor Khomenko and Roland Meyer.
   In Proceedings of ACSD 2009.
   DOI | PDF | BibTeX

8. Erasing in Petri Net Languages and Matrix Grammars, by Georg Zetzsche.
   In Proceedings of DLT 2009.
   DOI

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

6. Labeled Step Sequences in Petri Nets, by Matthias Jantzen and Georg Zetzsche.
   In Proceedings of PETRI NETS 2008.
   DOI

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

4. On boundedness in depth in the pi-calculus, by Roland Meyer.
   In Proceedings of IFIP TCS 2008.
   Slides | PDF | DOI | BibTeX

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

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

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