Reactive Systems Group

We develop algorithms and tools for the synthesis and verification of reactive systems.

Read our research profile
How to join us
Test our tools
Browse our publications

group photo of the Reactive System Group in front of a lake

Current Lectures

Winter 2022/23: Advanced Lecture Automata, Games and Verification

Summer 2022: Proseminar From Program Verification to Synthesis

Summer 2022: Seminar Neural-Symbolic Computing

Winter 2021: Core Lecture Verification

Summer 2021: Seminar Monitoring of Cyber-Physical Systems

Summer 2021: Proseminar Software Reliability

Winter 2020/21: Grundvorlesung Programmierung 1

Summer 2020: Seminar Neural-Symbolic Computing

Winter 2019/20: Advanced Lecture Reactive Synthesis

Winter 2019/20: Core Lecture Verification

Recent Publications

FSTTCS 2022: Synthesizing Dominant Strategies for Liveness
LICS 2022: Deciding Hyperproperties Combined with Functional Specifications
CSF 2022: Prophecy Variables for Hyperproperty Verification
ISSE 2022: Specification decomposition for reactive synthesis
ATVA 2022: Temporal Causality in Reactive Systems
CAV 2022: Software Verification of Hyperproperties Beyond k-Safety
CAV 2022: Explaining Hyperproperty Violations
CAV 2022: Information Flow Guided Synthesis
PLDI 2022: Can reactive synthesis and syntax-guided synthesis be friends?
HSCC 2022: BOCoSy: Small but Powerful Symbolic Output-Feedback Control.
ISSE 2022: Compositional synthesis of modular systems.
ISSE 2022: Live synthesis.
FoSSaCS 2022: Temporal Stream Logic modulo Theories.
CSL 2022: Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory.
FSTTCS 2021: Linear-time Temporal Logic with Team Semantics: Expressivity and Complexity.
ATVA 2021: Runtime Enforcement of Hyperproperties.
ATVA 2021: Compositional Synthesis of Modular Systems.
ATVA 2021: Live Synthesis.
VIS 2021: Visual Analysis of Hyperproperties for Understanding Model Checking Results.
CAV 2021: Causality-Based Game Solving.
NFM 2021: Specification Decomposition for Reactive Synthesis.
ICLR 2021: Teaching Temporal Logics to Neural Networks.
TACAS 2021: RTLola on Board: Testing Real Driving Emissions on your Phone.
TACAS 2021: A Web Interface for Petri Nets with Transits and Petri Games.
RV 2020: Verified Rust Monitors for Lola Specifications.
RV 2020: Automatic Optimizations for Stream-based Monitoring Languages.
RV 2020: Monitoring Cyber-Physical Systems: From Design to Integration..
ATVA 2020: Probabilistic Hyperproperties of Markov Decision Processes.
ATVA 2020: Explainable Reactive Synthesis.
ATVA 2020: Model Checking Branching Properties on Petri Nets with Transits.
ATVA 2020: Dependency-based Compositional Synthesis.
KR 2020: The Hierarchy of Hyperlogics: A Knowledge Reasoning Perspective.
CAV 2020: Realizing Omega-regular Hyperproperties.
CAV 2020: AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL.
CAV 2020: RTLola Cleared for Take-Off: Monitoring Autonomous Aircraft.
HSCC 2020: From LTL to rLTL Monitoring: Improved Monitorability through Robust Semantics.
ATVA 2019: Program Repair for Hyperproperties.
ATVA 2019: Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems.
ATVA 2019: Model Checking Data Flows in Concurrent Network Updates.
ATVA 2019: Approximate Automata for Omega-regular Languages.
EMSOFT 2019: FPGA Stream-Monitoring of Real-time Properties.
CONCUR 2019: Translating Asynchronous Games for Distributed Synthesis.
CAV 2019: Verifying Hyperliveness.
CAV 2019: Temporal Stream Logic: Synthesis beyond the Bools.
CAV 2019: StreamLAB: Stream-based Monitoring of Cyber-physical Systems.
CAV 2019: Synthesizing Approximate Implementations for Unrealizable Specifications.
SAT 2019: Clausal Abstraction for DQBF.
FMSD: Monitoring Hyperproperties.
CSF 2019: Canonical Representations of k-Safety Hyperproperties.
LICS 2019: The Hierarchy of Hyperlogics.
TACAS 2019: Constraint-based Monitoring of Hyperproperties.
ATVA 2018: Bounded Synthesis of Reactive Programs.
ATVA 2018: MGHyper: Checking Satisfiability of HyperLTL formulas beyond the ∃*∀* Fragment.
CSL 2018: Synthesizing Optimally Resilient Controllers.
CSL 2018: Parity Games with Weights.
MFCS 2018: Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems.
MFCS 2018: Team Semantics for the Specification and Verification of Hyperproperties.
CAV 2018: Model Checking Quantitative Hyperproperties.
CAV 2018: Synthesizing Reactive Systems from Hyperproperties.
CSF 2018: The Complexity of Monitoring Hyperproperties.
Acta Informatica: The Complexity of Counting Models of Linear-time Temporal Logic.
Acta Informatica: Parameterized Linear Temporal Logics Meet Costs: Still not Costlier than LTL.
TACAS 2018: RVHyper: A Runtime Verification Tool for Temporal Hyperproperties.
CCS 2017: Verifying Security Policies in Multi-agent Workflows with Loops.
IOS Press: Reactive Synthesis: Towards Output-Sensitive Algorithms.
FSTTCS 2017: Symmetric Synthesis.
FSTTCS 2017: Synthesis in Distributed Environments.
CREST 2017: Causality-based Model Checking.
Bulletin of EATCS: Temporal Hyperproperties.
ATVA 2017: The Density of Linear-time Properties.
LMCS: Easy to Win, Hard to Master: Optimal Strategies in Parity Games with Costs.
GandALF 2017: Finite-state Strategies in Delay Games.
RV 2017: Stream Runtime Monitoring on UAS.
RV 2017: Monitoring Hyperproperties.
CAV 2017: BoSy: An Experimentation Framework for Bounded Synthesis.
CAV 2017: EAHyper: Satisfiability, Implication, and Equivalence Checking of Hyperproperties.
CAV 2017: On Expansion and Resolution in CEGAR Based QBF Solving.
LICS 2017: Games with Costs and Delays.
ESOP 2017: Is your software on dope? ⋆ Formal analysis of surreptitiously “enhanced” programs.
Information and Computation: Parametric Linear Dynamic Logic.
TACAS 2017: Encodings of Bounded Synthesis.
AIAA Scitech 2017: Towards Intelligent System Health Management using Runtime Monitoring.
FOSSACS 2017: Bounding Average-energy Games.
STACS 2017: The First-order Logic of Hyperproperties.
RAIRO-ITA: Delay Games with WMSO+U Winning Conditions.
FSTTCS 2016: Visibly Linear Dynamic Logic.
FSTTCS 2016: Prompt Delay.
LMCS: How Much Lookahead is Needed to Win Infinite Games?
RV 2016: A Stream-based Specification Language for Network Monitoring.
ATVA 2016: Synthesizing Skeletons for Reactive Systems.
ATVA 2016: Specifying and Verifying Secrecy in Workflows with Arbitrarily Many Agents.
GandALF 2016: Approximating Optimal Bounds in Prompt-LTL Realizability in Doubly-exponential Time.
GandALF 2016: Distributed PROMPT-LTL Synthesis
CSL 2016: Easy to Win, Hard to Master: Optimal Strategies in Parity Games with Costs.
CONCUR 2016: Deciding Hyperproperties.
CAV 2016: Bounded Cycle Synthesis.
CAV 2016: Synthesis of Self-Stabilizing and Byzantine-Resilient Distributed Systems.
SAT 2016: Non-prenex QBF Solving Using Abstraction.
ACM SIGACT News: Decidability in Parameterized Verification.
RAIRO – ITA: Optimal Strategy Synthesis for Request-Response Games.
VMCAI 2016: Tight Cutoffs for Guarded Protocols with Fairness.
FMCAD 2015: CAQE: A Certifying QBF Solver.
Synthesis Lectures in Distributed Computing Theory: Decidability of Parameterized Verification.
GandALF 2015: Parameterized Linear Temporal Logics Meet Costs: Still not Costlier than LTL.
Correct System Design 2015: Bounded Synthesis for Petri Games.

more…