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 will start 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
- Core Lecture: Verification
Recent Publications
- 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.