Roland Meyer

CoRR, 2024

Realizability in Semantics-Guided Synthesis Done Eagerly.

[BibT_eX]

[DOI]

Jakob Tepe

CoRR, 2024

On the Separability Problem of VASS Reachability Languages.

[BibT_eX]

[DOI]

Eren Keskin

Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, 2024

Separability in Büchi VASS and Singly Non-Linear Systems of Inequalities.

[BibT_eX]

[DOI]

Proceedings of the 51st International Colloquium on Automata, Languages, and Programming, 2024

2023

Static Analysis of Memory Models for SMT Encodings.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., October, 2023

Embedding Hindsight Reasoning in Separation Logic.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2023

Context-Aware Separation Logic.

[BibT_eX]

[DOI]

CoRR, 2023

Contextual Equivalence for Alternation and Urgency.

[BibT_eX]

[DOI]

Eren Keskin

Sören van der Wall

CoRR, 2023

Make Flows Small Again: Revisiting the Flow Framework.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

Regular Separability in Büchi VASS.

[BibT_eX]

[DOI]

Pascal Baumann

Georg Zetzsche

Proceedings of the 40th International Symposium on Theoretical Aspects of Computer Science, 2023

Separability and Non-Determinizability of WSTS.

[BibT_eX]

[DOI]

Eren Keskin

Proceedings of the 34th International Conference on Concurrency Theory, 2023

nekton: A Linearizability Proof Checker.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 35th International Conference, 2023

2022

A concurrent program logic with a future and history.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2022

CAAT: consistency as a theory.

[BibT_eX]

[DOI]

Thomas Haas

Hernán Ponce de León

Proc. ACM Program. Lang., 2022

Liveness in broadcast networks.

[BibT_eX]

[DOI]

Prakash Saivasan

Computing, 2022

Dartagnan: SMT-based Violation Witness Validation (Competition Contribution).

[BibT_eX]

[DOI]

Hernán Ponce de León

Thomas Haas

Shankaranarayanan Krishna

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

Parameterized Verification under Release Acquire is PSPACE-complete.

[BibT_eX]

[DOI]

Adwait Godbole

Rafael Lourenco de Lima Chehab

Soham Chakraborty

Proceedings of the PODC '22: ACM Symposium on Principles of Distributed Computing, Salerno, Italy, July 25, 2022

Model-Based Fault Classification for Automotive Software.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems - 20th Asian Symposium, 2022

2021

Verifying and Optimizing Compact NUMA-Aware Locks on Weak Memory Models.

[BibT_eX]

[DOI]

Ming Fu

Shankara Narayanan Krishna

CoRR, 2021

Safety Verification of Parameterized Systems under Release-Acquire.

[BibT_eX]

[DOI]

Adwait Godbole

CoRR, 2021

Dartagnan: Leveraging Compiler Optimizations and the Price of Precision (Competition Contribution).

[BibT_eX]

[DOI]

Hernán Ponce de León

Thomas Haas

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2021

2020

Pointer life cycle types for lock-free data structures with memory reclamation.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2020

Fine-Grained Complexity of Safety Verification.

[BibT_eX]

[DOI]

Prakash Saivasan

J. Autom. Reason., 2020

Dartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution).

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2020

On the State Reachability Problem for Concurrent Programs Under Power.

[BibT_eX]

[DOI]

Proceedings of the Networked Systems - 8th International Conference, 2020

On the Complexity of Multi-Pushdown Games.

[BibT_eX]

[DOI]

Sören van der Wall

Proceedings of the 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2020

2019

Decoupling lock-free data structures from memory reclamation for static analysis.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2019

Sicherheit, Zuverlässigkeit, Korrektheit.

[BibT_eX]

[DOI]

Juliane Krämer

Proceedings of the 49. Jahrestagung der Gesellschaft für Informatik, 50 Jahre Gesellschaft für Informatik, 2019

Complexity of Liveness in Parameterized Systems.

[BibT_eX]

[DOI]

Prakash Saivasan

Proceedings of the 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2019

Temporal Tracing of On-Chip Signals using Timeprints.

[BibT_eX]

[DOI]

Proceedings of the 56th Annual Design Automation Conference 2019, 2019

BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

Inductive Counting and the Reachability Problem for Petri Nets.

[BibT_eX]

[DOI]

Proceedings of the Carl Adam Petri: Ideas, Personality, Impact, 2019

2018

Fast Witness Counting.

[BibT_eX]

[DOI]

CoRR, 2018

Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems.

[BibT_eX]

[DOI]

Proceedings of the 43rd International Symposium on Mathematical Foundations of Computer Science, 2018

BMC with Memory Models as Modules.

[BibT_eX]

[DOI]

Proceedings of the 2018 Formal Methods in Computer Aided Design, 2018

Bounded Context Switching for Valence Systems.

[BibT_eX]

[DOI]

Georg Zetzsche

Proceedings of the 29th International Conference on Concurrency Theory, 2018

Regular Separability of Well-Structured Transition Systems.

[BibT_eX]

[DOI]

Proceedings of the 29th International Conference on Concurrency Theory, 2018

Reasoning About Weak Semantics via Strong Semantics.

[BibT_eX]

[DOI]

Proceedings of the Principled Software Development, 2018

2017

Message from the Guest Editors.

[BibT_eX]

[DOI]

Stefan Haar

ACM Trans. Embed. Comput. Syst., 2017

Liveness Verification and Synthesis: New Algorithms for Recursive Programs.

[BibT_eX]

[DOI]

Elisabeth Neumann

CoRR, 2017

Portability Analysis for Axiomatic Memory Models. PORTHOS: One Tool for all Models.

[BibT_eX]

[DOI]

CoRR, 2017

Effect Summaries for Thread-Modular Analysis.

[BibT_eX]

[DOI]

CoRR, 2017

Portability Analysis for Weak Memory Models. PORTHOS: One Tool for all Models.

[BibT_eX]

[DOI]

Proceedings of the Static Analysis - 24th International Symposium, 2017

Effect Summaries for Thread-Modular Analysis - Sound Analysis Despite an Unsound Heuristic.

[BibT_eX]

[DOI]

Proceedings of the Static Analysis - 24th International Symposium, 2017

Locality and Singularity for Store-Atomic Memory Models.

[BibT_eX]

[DOI]

Sebastian Schweizer

Proceedings of the Networked Systems - 5th International Conference, 2017

Domains for Higher-Order Games.

[BibT_eX]

[DOI]

Matthew Hague

Proceedings of the 42nd International Symposium on Mathematical Foundations of Computer Science, 2017

On the Upward/Downward Closures of Petri Nets.

[BibT_eX]

[DOI]

Proceedings of the 42nd International Symposium on Mathematical Foundations of Computer Science, 2017

On the Complexity of Bounded Context Switching.

[BibT_eX]

[DOI]

Proceedings of the 25th Annual European Symposium on Algorithms, 2017

2016

Munchausen Iteration.

[BibT_eX]

[DOI]

CoRR, 2016

Antichains for Inclusion Games.

[BibT_eX]

[DOI]

Lukás Holík

CoRR, 2016

On the Complexity of Bounded Context Switching.

[BibT_eX]

[DOI]

CoRR, 2016

Pointer Race Freedom.

[BibT_eX]

[DOI]

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2016

First-order logic with reachability for infinite-state systems.

[BibT_eX]

[DOI]

Emanuele D'Osualdo

Georg Zetzsche

Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

Summaries for Context-Free Games.

[BibT_eX]

[DOI]

Lukás Holík

Proceedings of the 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2016

2015

Memory-Model-Aware Testing: A Unified Complexity Analysis.

[BibT_eX]

[DOI]

Florian Furbach

Klaus Schneider

Maximilian Senftleben

ACM Trans. Embed. Comput. Syst., 2015

Antichains for the Verification of Recursive Programs.

[BibT_eX]

[DOI]

Lukás Holík

Proceedings of the Networked Systems - Third International Conference, 2015

What's Decidable about Availability Languages?.

[BibT_eX]

[DOI]

Proceedings of the 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, 2015

Lazy TSO Reachability.

[BibT_eX]

[DOI]

Proceedings of the Fundamental Approaches to Software Engineering, 2015

From Program Verification to Time and Space: The Scientific Life of Ernst-Rüdiger Olderog.

[BibT_eX]

[DOI]

Heike Wehrheim

Proceedings of the Correct System Design, 2015

2014

Robustness against Relaxed Memory Models.

[BibT_eX]

[DOI]

Proceedings of the Software Engineering 2014, Fachtagung des GI-Fachbereichs Softwaretechnik, 25. Februar, 2014

Robustness against Power is PSpace-complete.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages, and Programming - 41st International Colloquium, 2014

Bounds on Mobility.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2014 - Concurrency Theory - 25th International Conference, 2014

2013

A Polynomial Translation of pi-calculus FCPs to Safe Petri Nets.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2013

Static Provenance Verification for Message Passing Programs.

[BibT_eX]

[DOI]

Zilong Wang

Proceedings of the Static Analysis - 20th International Symposium, 2013

Provenance Verification.

[BibT_eX]

[DOI]

Zilong Wang

Proceedings of the Reachability Problems - 7th International Workshop, 2013

A Theory of Partitioned Global Address Spaces.

[BibT_eX]

[DOI]

Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2013

Checking and Enforcing Robustness against TSO.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2013

A Theory of Name Boundedness.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2013 - Concurrency Theory - 24th International Conference, 2013

2012

Petri Net Reachability Graphs: Decidability Status of First Order Properties

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2012

Robustness Checking against TSO: Attacks and Defence

[BibT_eX]

[DOI]

CoRR, 2012

Language-Theoretic Abstraction Refinement.

[BibT_eX]

[DOI]

Proceedings of the Fundamental Approaches to Software Engineering, 2012

A Polynomial Translation of π-Calculus (FCP) to Safe Petri Nets.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2012 - Concurrency Theory - 23rd International Conference, 2012

An Algorithmic Framework for Coverability in Well-Structured Systems.

[BibT_eX]

[DOI]

Tim Strazny

Proceedings of the 12th International Conference on Application of Concurrency to System Design, 2012

2011

Deciding Robustness against Total Store Ordering.

[BibT_eX]

[DOI]

Eike Möhlmann

Proceedings of the Automata, Languages and Programming - 38th International Colloquium, 2011

Petri Net Reachability Graphs: Decidability Status of FO Properties.

[BibT_eX]

[DOI]

Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2011

2010

The Downward-Closure of Petri Net Languages.

[BibT_eX]

[DOI]

Peter Habermehl

Harro Wimmel

Proceedings of the Automata, Languages and Programming, 37th International Colloquium, 2010

Kleene, Rabin, and Scott Are Available.

[BibT_eX]

[DOI]

Jochen Hoenicke

Ernst-Rüdiger Olderog

Proceedings of the CONCUR 2010 - Concurrency Theory, 21th International Conference, 2010

Petruchio: From Dynamic Networks to Nets.

[BibT_eX]

[DOI]

Tim Strazny

Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

2009

Structural stationarity in the π-calculus.

[BibT_eX]

[DOI]

PhD thesis, 2009

A Practical Approach to Verification of Mobile Systems Using Net Unfoldings.

[BibT_eX]

[DOI]

Tim Strazny

Fundam. Informaticae, 2009

A theory of structural stationarity in the <i>pi</i> -Calculus.

[BibT_eX]

[DOI]

Acta Informatica, 2009

Strukturelle Stationarität.

[BibT_eX]

[DOI]

Proceedings of the Ausgezeichnete Informatikdissertationen 2009, 2009

On the Relationship between π-Calculus and Finite Place/Transition Petri Nets.

[BibT_eX]

[DOI]

Roberto Gorrieri

Proceedings of the CONCUR 2009 - Concurrency Theory, 20th International Conference, 2009

Checking pi-Calculus Structural Congruence is Graph Isomorphism Complete.

[BibT_eX]

[DOI]

Proceedings of the Ninth International Conference on Application of Concurrency to System Design, 2009

2008

Model checking Duration Calculus: a practical approach.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2008

On Boundedness in Depth in the pi-Calculus.

[BibT_eX]

[DOI]

Proceedings of the Fifth IFIP International Conference On Theoretical Computer Science, 2008

2006

Trustworthy software systems: a discussion of basic concepts and terminology.

[BibT_eX]

[DOI]

ACM SIGSOFT Softw. Eng. Notes, 2006

Model Checking Duration Calculus: A Practical Approach.

[BibT_eX]

[DOI]

Johannes Faber

Andrey Rybalchenko

Proceedings of the Theoretical Aspects of Computing, 2006

Model Checking Data-Dependent Real-Time Properties of the European Train Control System.

[BibT_eX]

[DOI]

Johannes Faber