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 on the programme committees of CAV 2014 and ICE 2014, and on the editorial board of Acta Informatica. If you would like me to handle your Acta Informatica submission, please send me e-mail.
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).
- Detecting Unrealizable Specifications of Distributed Systems. With Leander Tentrup. To appear at TACAS 2014
- Temporal Logics for Hyperproperties. With Michael R. Clarkson, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and Cesar Sanchez. To appear at POST 2014
- Counting Models of Linear-time Temporal Logic. With Hazem Torfah. To appear at LATA 2014
- Monitoring Parametric Temporal Logic. With Peter Faymonvolle and Doron Peled. To appear at 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.