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
    Functional Programming and Verification
    Core Lecture · Summer 2026
    The course provides an introduction to functional programming and program verification. We use the programming language OCaml to study the fundamental concepts of functional programming. We cover notions like recursion, higher-order functions, polymorphic types, and constructors, as well as static and dynamic semantics and the verification of functional programs.
    Organized by: Bernd Finkbeiner, Iona Kuhn, Julian Erhard, N. Ege Saraç, Aleksy Feliks Idzikowski, Alexander Glas, Manuel Lerchner, Aziz Abderrahmane Ben Othmane, Cihan Demirci, Conrad Laurenz Fischer, Darina Grigoriu, Ferdinand Schenk, Ilya Kats, Leonie Houzer, Leopold Cario, Matei-Alexandru Florescu, Paul Schadauer, Tjorben Huber, Tobias Vale and Yi Rui Cui Visit Course
    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
Contact Data Privacy Policy Imprint
Home People Publications
More