Bernd Finkbeiner

Bernd Finkbeiner Reactive Systems Group Universität des Saarlandes Phone: +49 681 302 5632 eMail: finkbeiner at cs.uni-sb.de Building: E 1 3 Room: 506 Coordinates: N 49.257833° E 7.045144°

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).

• Automata-theoretic synthesis of reactive systems, for example: uniform distributed synthesis
• Automata-theoretic verification of reactive systems, for example: language containment checking
• Constraint-based abstraction of reactive systems, for example: slicing abstractions
• Stream-based runtime analysis of reactive systems, for example: runtime monitoring

• See also: Reactive Systems Group – Research – Publications

Teaching

• Core lecture course: Embedded Systems. Embedded systems are computer systems that are encapsulated into larger products, and that are normally not directly visible to the user. Embedded systems are responsible for the information processing in transportation systems (e.g., airplanes, trains, cars), telecommunication equipment (e.g., mobile phones), and consumer electronics products (e.g., TVs, DVD-players). In this course we will study the theoretical foundations and practical tools that are needed to build reliable and efficient embedded systems.

Publications

• Bounded Synthesis. With Sven Schewe. STTT 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. 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.