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
Teaching
- Winter 2024/25: Advanced Lecture Automata, Games and Verification
- Summer 2024: Seminar Neural-Symbolic Computing
- Winter 2023: Core Lecture Verification
- Summer 2023: Seminar Hyperproperties
- 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
Recent Publications
- NeurIPS 2024: Learning Better Representations from Less Data for Propositional Satisfiability
- CAV 2024: Information Flow Guided Synthesis with Unbounded Communication
- CAV 2024: Synthesis of Temporal Causality
- ICAPS 2024: Non-Deterministic Planning for Hyperproperty Verification
- AAMAS 2024: Hyper Strategy Logic
- AAMAS 2024: Monitoring Second-Order Hyperproperties
- TACAS 2024: Automated Software Verification of Hyperliveness
- TACAS 2024: NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis
- AAAI 2024: On Alternating-Time Temporal Logic, Hyperproperties, and Strategy Sharing
- ACM SIGLOG News: Logics and Algorithms for Hyperproperties
- CAV 2023: nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models
- CAV 2023: Second-Order Hyperproperties
- CSF 2023: Smart Contract Synthesis Modulo Hyperproperties
- LPAR 2023: Counterfactuals Modulo Temporal Logics
- ICLR 2023: Iterative Circuit Repair Against Formal Specifications
- 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
- RV 2022: Real-time Visualization of Stream-based Monitoring Data
- 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.