I am a professor in computer science at Saarland University. I am currently the chairman of the examination board. If you have questions regarding the examination regulations please come to my office hours on Wednesdays 3-4pm.
I am co-chair of the program committee of ATVA 2015, member of the program committees of RV 2016 and SYNT 2016, and member of the editorial board of Acta Informatica.
I am interested in computer systems and protocols that are reactive in nature: systems of concurrent processes that interact with each other and with their environment over a possibly infinite run. Parallelism and nondeterminism make it difficult to design such systems correctly. My research concerns computer-aided methods that derive implementations from formal specifications (synthesis) and that prove that a given implementation satisfies a logical property (verification).
- Automatic verification of reactive systems,
for example: causal termination
- Automatic synthesis of reactive systems,
for example: synthesis of reactive systems
- Automatic information flow analysis of reactive systems,
for example: HyperLTL and HyperCTL*
- Automatic runtime analysis of reactive systems,
for example: runtime monitoring.
- Is your software on dope? ⋆ Formal analysis of surreptitiously “enhanced” programs. With Pedro R. D’Argenio, Gilles Barthe, Sebastian Biewer, and Holger Hermanns. ESOP 2017.
- Encodings of Bounded Synthesis. With Peter Faymonville, Markus N. Rabe, and Leander Tentrup, TACAS 2017.
- The First-Order Logic of Hyperproperties. With Martin Zimmermann, STACS 2017.
- Facets of Software Doping. With Gilles Barthe, Pedro R. D’Argenio, and Holger Hermanns. ISOLA 2016.
- Petri games: Synthesis of distributed systems with causal memory. With Ernst-Rüdiger Olderog. Information & Computation
- A Stream-based Specification Language for Network Monitoring. With Peter Faymonville, Sebastian Schirmer, and Hazem Torfah. RV 2016
- Deciding Hyperproperties. With Christopher Hahn. CONCUR 2016
- Specifying and Verifying Secrecy in Workflows with Arbitrarily Many Agents. With Helmut Seidl and Christian Müller. ATVA 2016
- Synthesizing Skeletons for Reactive Systems. With Hazem Torfah. ATVA 2016
- Bounded Cycle Synthesis. With Felix Klein. CAV 2016
- Synthesis of Reactive Systems. Dependable Software Systems Engineering
- Bounded Synthesis for Petri Games. Correct System Design 2015.
- Detecting Unrealizability of Distributed Fault-tolerant Systems. With Leander Tentrup. Accepted at LMCS.
- Algorithms for Model Checking HyperLTL and HyperCTL*. With Markus Rabe and César Sánchez. CAV 2015.
- ADAM: Causality-Based Synthesis of Distributed Systems. With Manuel Gieseking and Ernst-Rüdiger Olderog. CAV 2015.
- Petri Games: Synthesis of Distributed Systems with Causal Memory. With Ernst-Rüdiger Olderog. To appear at GANDALF 2014.
- Fast DQBF Refutation. With Leander Tentrup. SAT 2014.
- Causal Termination of Multi-threaded Programs. With Andrey Kupriyanov. CAV 2014.
- Automatic Compositional Synthesis of Distributed Systems. With Werner Damm. FM 2014.
- Detecting Unrealizable Specifications of Distributed Systems. With Leander Tentrup. TACAS 2014.
- Temporal Logics for Hyperproperties. With Michael R. Clarkson, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and Cesar Sanchez. POST 2014.
- Counting Models of Linear-time Temporal Logic. With Hazem Torfah. LATA 2014.
- Monitoring Parametric Temporal Logic. With Peter Faymonville and Doron Peled. VMCAI 2014.
- Relational Abstract Interpretation for the Verification of 2-Hypersafety Properties. With Máté Kovács and Helmut Seidl. CCS 2013
- Bounded Synthesis. With Sven Schewe. STTT 2013
- Causality-Based Verification of Multi-threaded Programs. With Andrey Kupriyanov. CONCUR 2013
- A Temporal Logic for Hyperproperties. With Markus N. Rabe and César Sánchez. arXiv.
- Lossy Channel Games under Incomplete Information. With Rayna Dimitrova. SR 2013.
- Efficient Parallel Path Checking for Linear-Time Temporal Logic With Past and Bounds. With Lars Kuhtz. LMCS 2012
- Monitoring Temporal Information Flow with Rayna Dimitrova and Markus N. Rabe, ISOLA 2012
- The Complexity of Bounded Synthesis for Timed Control with Partial Observability with Hans-Jörg Peter, FORMATS 2012
- Counterexample-guided Synthesis of Observation Predicates with Rayna Dimitrova, FORMATS 2012
- Template-based Controller Synthesis for Timed Systems. With Hans-Jörg Peter. TACAS 2012
- Lazy Synthesis. With Swen Jacobs. VMCAI 2012
- Model Checking Information Flow in Reactive Systems. With Rayna Dimitrova, Máté Kovács, Markus N. Rabe, and Helmut Seidl. RS3 Best Paper Award. VMCAI 2012
- Monitoring Realizability. With Rüdiger Ehlers. RV 2011
- Weak Kripke Structures and LTL. With Lars Kuhtz. CONCUR 2011
- Does It Pay to Extend the Perimeter of a World Model? With Werner Damm. FM 2011
- Reactive Safety. With Rüdiger Ehlers. GANDALF 2011
- On the Virtue of Patience: Minimizing Büchi Automata. With Rüdiger Ehlers. SPIN 2010
- Model Checking the FlexRay Physical Layer Protocol. With Michael Gerke, Rüdiger Ehlers, and Hans-Jörg Peter. FMICS 2010
- Coordination Logic. With Sven Schewe. CSL 2010
- Synthesising Certificates in Networks of Timed Automata. With Hans-Jörg Peter and Sven Schewe. IET Software 2010
- SLAB: A Certifying Model Checker for Infinite-State Concurrent Systems. TACAS 2010
- Synthesis of Fault-Tolerant Distributed Systems. With Rayna Dimitrova. ATVA 2009
- LTL Path Checking is Efficiently Parallelizable. With Lars Kuhtz. Best Paper Award. ICALP 2009
- Monitor Circuits for LTL with Bounded and Unbounded Future. With Lars Kuhtz. RV 2009
- Slicing Abstractions. With Ingo Brückner, Klaus Dräger, and Heike Wehrheim. FI 2008.
- Abstraction Refinement for Games with Incomplete Information. With Rayna Dimitrova. FSTTCS 2008
- Synthesizing Certificates in Networks of Timed Automata. With Hans-Jörg Peter and Sven Schewe. RTSS 2008
- Directed Model Checking with Distance-preserving Abstractions. With Klaus Dräger and Andreas Podelski. STTT 2008
- Subsequence Invariants. With Klaus Dräger. CONCUR 2008
- RESY: Requirement Synthesis for Compositional Model Checking. With Hans-Jörg Peter and Sven Schewe. TACAS 2008
- UPPAAL/DMC – Abstraction-based Heuristics for Directed Model Checking. With Sebastian Kupferschmid, Klaus Dräger, Jörg Hoffmann, Henning Dierks, Andreas Podelski, and Gerd Behrmann. TACAS 2007
- SMT-Based Synthesis of Distributed Systems. With Sven Schewe. AFM 2007
- Distributed Synthesis for Alternating-Time Logics. With Sven Schewe. ATVA 2007
- Slicing Abstractions. With Ingo Brückner, Klaus Dräger, Bernd Finkbeiner, and Heike Wehrheim. Best Paper Award. FSEN 2007
- Bounded Synthesis. With Sven Schewe. ATVA 2007
- Semi-Automatic Distributed Synthesis. With Sven Schewe. JFCS 2007
- Automatic Synthesis of Assumptions for Compositional Model Checking. With Sven Schewe and Matthias Brill. FORTE 2006
- Satisfiability and Finite Model Property for the Alternating-Time µ-Calculus. With Sven Schewe. CSL 2006
- Synthesis of Asynchronous Systems. With Sven Schewe. LOPSTR 2006.
- Directed Model Checking with Distance-Preserving Abstractions. With Klaus Dräger and Andreas Podelski. SPIN 2006
- Semi-Automatic Distributed Synthesis. With Sven Schewe. ATVA 2005
- Uniform Distributed Synthesis. With Sven Schewe. LICS 2005
- LOLA: Runtime Monitoring of Synchronous Systems. With Ben d’Angelo, Sriram Sankaranarayanan, Cesar Sanchez, Will Robinson, Henny B. Sipma, Sandeep Mehrotra, Zohar Manna. TIME 2005
- Collecting Statistics over Runtime Executions. With Sriram Sankaranarayanan and Henny Sipma. FMSD 2005
- Checking Finite Traces using Alternating Automata. With Sriram Sankaranarayanan and Henny Sipma. FMSD 2004
- Collecting Statistics over Runtime Executions. With Henny Sipma. RV 2002
- Using Message Sequence Charts for Component-Based Formal Verification. With Ingolf Krüger. SAVCBS 2001.
- Checking Finite Traces using Alternating Automata. With Henny Sipma. RV 2001
- Language Containment Checking with Nondeterministic BDDs. TACAS 2001
- The `Cash-Point Service: A Verification Case Study Using STeP
With Anca Browne, Zohar Manna and Henny Sipma. FAC 2000.
- Verifying Temporal Properties of Reactive Systems: A STeP Tutorial.
With Nikolaj S. Bjørner, Anca Browne, Michael A. Colón, Zohar Manna, Henny B. Sipma and Tomás E. Uribe. FMSD 2000
- An Update on STeP: Deductive-Algorithmic Verification of Reactive Systems.
With Zohar Manna, Nikolaj S. Bjørner, Anca Browne, Michael A. Colón, Bernd Finkbeiner, Mark Pichora, Henny B. Sipma and Tomás E. Uribe. TOOLS 1999
- Abstraction and Modular Verification of Infinite-State Reactive Systems.
With Zohar Manna, Michael A. Colón, Henny B. Sipma and Tomás E. Uribe. RTSE 1998
- Deductive Verification of Modular Systems
With Zohar Manna and Henny B. Sipma. COMPOS 1997.