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
We have moved!
Visit us in our new offices in building E1.1
ERC project OSARES
The OSARES project has started in July 2016. The goal of the project is the automatic synthesis of distributed embedded systems — that is, the construction of computer programs for such systems by a computer without the help of a human programmer. The project is funded by the European Research Council for five years, from 2016 to 2021, as an ERC Consolidator Grant. more…
Current lectures
- Block Seminar: Runtime Verification
- Core Lecture: Verification
Recent Publications
- 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.