|Reactive Systems Group
Universität des Saarlandes
Phone: +49 681 302 5651
eMail: finkbeiner at cs.uni-saarland.de
Office hour: Wednesdays, 3-4pm
Building: E1 1 Room: 1.11
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.
I am currently the chairman of the examination boards for Computer Science B.Sc., M.Sc. and Applied Computer Science, for Computer and Communications Technology, and for Embedded Systems. If you have an examination issue or a question that needs to be addressed by one of these boards, please send me a message or see me in my office hour (Wednesdays, 3-4pm).
- Proseminar: Formal Verification of Security Protocols.
Security protocols are omnipresent in our daily lives in areas such as online banking and mobile phones. Their purpose is to keep our transactions and personal data secure. Because these protocols are implemented on potentially insecure networks like the internet, they are notoriously difficult to devise. The field of formal analysis of security protocols has seen significant advances during the last years. There is now a better understanding of decidability and complexity questions, and models with solid theoretical foundations have been developed together with proof techniques. Automated tools based on these insights have been designed and successfully applied to numerous protocols, including industrial protocols. In this Proseminar, we will look at the recent and ongoing work in this very active field of research.
- Core Lecture: Embedded Systems.
When asked about computers and processors most people immediately imagine a laptop or a PC sitting under a desk. In reality, however, only a small fraction of processors are actually used for such systems. The major part is used as embedded components in larger systems, often not directly visible to the user.
They control everyday devices such as TVs, microwaves, and alarm clocks, but also highly safety-critical systems like air control, nuclear reactor control, automatic defibrillators, and robotic surgery-assistance systems.
Embedded systems often interact with the real world. An automatic thermostat gets information about the environment by sensing the room temperature and actively changes the environment by turning on the heater. This introduces several new challenges such as real-time dependent control and noise in input data.
In this course, we will have a closer look at the theoretical and practical aspects of designing reliable embedded systems. The theoretical foundations studied in this course are complemented by a practical project. Here, participants can immediately experience and overcome emerging problems discussed in theory.
- Lectures on reactive synthesis at the Winter School on Formal Verification 2017
- Tutorials at RV 2016 and FMCAD 2016 on hyperproperties
- Temporal Hyperproperties
- Reactive Synthesis: Towards Output-Sensitive Algorithms
- Causality-based Model Checking
- Bounded Synthesis of Reactive Programs. With Carsten Gerstacker and Felix Klein. Accepted at ATVA 2018
- MGHyper: Checking Satisfiability of HyperLTL formulas beyond the exists-forall Fragment. With Christopher Hahn and Tobias Hans. Accepted at ATVA 2018
- Synthesizing Reactive Systems from Hyperproperties. With Christopher Hahn, Philip Lukert, Marvin Stenger, and Leander Tentrup. CAV 2018
- Model Checking Quantitative Hyperproperties. With Christopher Hahn and Hazem Torfah. CAV 2018
- The Complexity of Monitoring Hyperproperties. With Borzoo Bonakdarpour. CSF 2018
- RVHyper: A Runtime Verification Tool for Temporal Hyperproperties. With Christopher Hahn, Marvin Stenger, and Leander Tentrup. TACAS 2018
- Symmetric Synthesis. With Ruediger Ehlers. FSTTCS 2017
- Synthesis in Distributed Environments. With Paul Gölz. FSTTCS 2017
- Verifying Security Policies in Multi-agent Workflows with Loops. With Christian Müller, Eugen Zalinescu, and Helmut Seidl. CCS 2017
- Reactive Synthesis: Towards Output-Sensitive Algorithms. With Felix Klein. Dependable Software Systems Engineering 2017
- Causality-based Model Checking. With Andrey Kupriyanov. Invited paper. CREST 2017
- Temporal Hyperproperties. Bulletin of EATCS No 123, October 2017
- Density of Linear-time Properties. With Hazem Torfah. ATVA 2017
- Monitoring Hyperproperties. With Christopher Hahn, Marvin Stenger, and Leander Tentrup. RV 2017
- Stream Runtime Monitoring on UAS. With Florian-Michael Adolf, Peter Faymonville, Sebastian Schirmer, and Christoph Torens. RV 2017
- EAHyper: Satisfiability, Implication, and Equivalence Checking of Hyperproperties. With Christopher Hahn and Marvin Stenger. CAV 2017
- BoSy: An Experimentation Framework for Bounded Synthesis. With Peter Faymonville and Leander Tentrup. CAV 2017
- Vehicle Platooning Simulations with Functional Reactive Programming. With Felix Klein, Ruzica Piskac and Mark Santolucito. SCAV@CPSWeek 2017
- 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
- Petri games: Synthesis of distributed systems with causal memory. With Ernst-Rüdiger Olderog. Information & Computation, 2017
- Facets of Software Doping. With Gilles Barthe, Pedro R. D’Argenio, and Holger Hermanns. ISOLA 2016
- A Stream-based Specification Language for Network Monitoring. With Peter Faymonville, Sebastian Schirmer, and Hazem Torfah. RV 2016
- What You Really Need To Know About Your Neighbor. With Werner Damm and Astrid Rakow. SYNT 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. LMCS 2015
- 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. 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.