Bernd Finkbeiner

Prof. Bernd Finkbeiner, Ph.D. is a faculty member at the CISPA Helmholtz Center for Information Security and a professor of computer science at Technical University of Munich. He obtained his Ph.D. in 2003 from Stanford University. Since 2003, he leads the Reactive Systems Group, which became part of CISPA in 2020. His research focus is the development of reliable guarantees for the safety and security of computer systems, including specification, program synthesis and repair, and static and dynamic verification. Major projects include output-sensitive algorithms for reactive synthesis, logics and algorithms for hyperproperties, and the stream-based monitoring of cyber-physical systems.

Project Hyper

ERC Advanced Grant 2022-2027

finkbeiner@cispa.de

+49 681 87083 2059

CISPA, Saarbrücken

E9 1 / 1.08

Teaching

Coinductive Proofs

Advanced lecture · Summer 2025

Proofs by induction appear everywhere in theoretical computer science; you certainly encountered them on many occasions, starting with the lecture Programming 1. Another essential proof method, less well-known but equally useful, is coinduction.

Organized by: Arthur Correnson, Bernd Finkbeiner and Iona Kuhn Visit Course

Automata, Games and Verification

Advanced lecture · Winter 2024/2025

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 will study the main ingredients of this elegant theory, and its application to automatic verification (model checking) and program synthesis.

Organized by: Bernd Finkbeiner, Vladimir Krsmanovic, Nico Mansion and Mihir Vahanwala Visit Course

Neural-Symbolic Computing

Seminar · Summer 2024

The way our brain forms thoughts can be classified into two categories (according to Kahneman in his book “Thinking Fast and Slow”): System 1: fast, automatic, frequent, stereotypic, unconscious (e.g. "Is this a cat or a dog?" or "What does this sentence mean in English?") and System 2: slow, effortful, logical, conscious (e.g. "17*16 = ?" or "If a -> b does b -> a?"). The traditional view is that deep learning is limited to System 1 type of reasoning. Mostly because of the perception that deep neural networks are unable to solve complex logical reasoning tasks reliably. Historically, applications of machine learning were thus often restricted to sub-problems within larger logical frameworks, such as resolving heuristics in solvers. In this seminar, we will explore new research that shows that deep neural networks are, in fact, able to reason on “symbolic systems”, i.e., systems that are built with symbols like programming languages or formal logics.

Organized by: Mohamed Ghanem, Matthias Cosler, Bernd Finkbeiner and Mihir Vahanwala Visit Course

Tutorial Videos

Overview Papers

Künstliche Intelligenz in der Softwareentwicklung: Über die Schulter geschaut.

iX Magazin für professionelle Informationstechnik 8/2021 (in German)

Selected Publications

Contact Data Privacy Policy Imprint

Home People Publications