|
Contact Jobs
|
Bernd Finkbeiner
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.
Research
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).
Teaching
- Summersemester 2011: Automata, Games and Verification.
The theory of automata over infinite objects provides a succinct, expressive and formal framework for reasoning about reactive systems, such as communication protocols and control systems. Reactive systems are characterized by their nonterminating behaviour and persistent interaction with their environment. In this course we study the main ingredients of this elegant theory, and its application to automatic verification (model checking) and program synthesis.
- Summersemester 2011: Games, Synthesis and Robotics.
In this seminar, we will explore the theory and applications of infinite games. In particular, we consider the automatic synthesis of control software for robots. We offer seminar topics broadly classifiable into two categories: Foundational aspects, i.e. game solving, variants of synthesis and temporal logic and applied aspects, i.e. robotic control software in combination with our hardware platform, three e-puck robots.
Publications
- 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.
|
|