Reactive Systems Group

Get In Touch! We are always looking for talented students and researchers to join our team. Check out our research areas and student projects to learn more about what we do.

Student Projects Research Areas
The members of the Reactive Systems Group

Research & Grants

Learn more
Hyperproperties
Hyperproperties
Reactive Synthesis
Reactive Synthesis
Runtime Monitoring
Runtime Monitoring
Neuro-symbolic Formal Methods
Neuro-symbolic Formal Methods
Grant 2022–2027
HYPER
Logics and Algorithms for a Unified Theory of Hyperproperties
ERC Advanced Grant
Grant 2024–2026
PreCePT
Precise Monitoring of Cyber-Physical Technology under Uncertainty
Grant 2019–2026
CPEC
Center for Perspicuous Computing – Distributed Knowledge and Information Flow
Transregional Collaborative Research Centre
Grant 2020–2023
Knowledge-based Synthesis
GIF Research Grant Regular Program
Grant 2020–2023
VoloSTreAM
Reliable runtime monitoring by means of traceable status analysis for highly critical eVOTL operation
Grant 2016–2021
OSARES
Output-Sensitive Algorithms for Reactive Synthesis
ERC Consolidator Grant

People

Meet everyone
Bernd Finkbeiner
Bernd Finkbeiner
Jan Baumeister
Jan Baumeister
Raven Beutner
Raven Beutner
Norine Coenen
Norine Coenen
Arthur Correnson
Arthur Correnson
Matthias Cosler
Matthias Cosler
Julian Erhard
Julian Erhard
Mohamed Ghanem
Mohamed Ghanem
Florian Kohn
Florian Kohn
Vladimir Krsmanovic
Vladimir Krsmanovic
Iona Kuhn
Iona Kuhn
Nico Mansion
Nico Mansion
N. Ege Saraç
N. Ege Saraç
Frederik Scheerer
Frederik Scheerer
Frederik Schmitt
Frederik Schmitt
Julian Siber
Julian Siber

Featured Publications

Show all

Teaching

Show all
    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
Contact Data Privacy Policy Imprint
Home People Publications
More