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
Busy Beaver 2018
The 2017/2018 edition of our lecture Programmierung 1 has received the Busy Beaver award for outstanding teaching performance.
Current Lectures
- Winter 2019/20: Core Lecture Verification
- Summer 2019: Block Seminar Hybrid Systems
- Summer 2019: Proseminar Softwarezuverlässigkeit
- Winter 2018/19: Advanced Lecture Automata, Games and Verification
- Winter 2018/19: Seminar Hyperproperties
Recent Publications
- 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.