Reactive systems are computer systems that maintain a continuous interaction with the environment in which they execute. Examples of reactive systems are controllers embedded in cars or planes, system level software, device drivers, communication protocols, etc. On the one hand, those systems are notoriously difficult to develop correctly (because of characteristics like concurrency, real-time constraints, parallelism, etc). And on the other hand, their correctness is often critical as they are used in contexts where safety is an issue, or because of economical reasons related to mass production.
To ensure reliability of reactive systems, advanced verification techniques have been developed. One particularly successful approach is model-checking. Nevertheless, model-checking is used to find bugs in designs but it does not support the design itself.
In this project, we want to develop new algorithms and tools to support the automatic synthesis of modern reactive systems (instead of their verification a posteriori). We aim at a shift from verification to synthesis. To allow this shift, we need new foundations: we propose to generalize transition systems and automata – models of computation in the classical approach to verification – by the more flexible and richer game-theoretic framework. Our work will be of fundamental nature but will also aim at the development of algorithms and prototypes of tools. Those new foundations will allow for the development of a new generation of computer-aided design tools that will support the automatic synthesis of modern reactive systems and ensure correctness by construction.Start date: January 1st, 2012.
Duration: 5 years.
Positions: several PhD and Post-Doc positions will be open soon. Here is a non-exhaustive list of possible topics:
- Games with imperfect information
- New solution concepts for synthesis
- Quantitative game models for reactive systems
- Algorithms for game theory
- Current researchers:
- Former members:
- AbsSynthe is an
open-source synthesis tool. It takes as input safety specifications in the
extended AIGER format and determines whether synthesizing a circuit to realize
the specification is possible. If this is the case, the tool outputs the
desired circuit also in AIGER format. AbsSynthe placed first in the
sequential synthesis track
of the 2014 synthesis competition in 2014,
SyntComp. The competition was
part of the
FLoC Olympic Games.
The team was awarded a Kurt Gödel medal in silver for this achievement.
Copyright (C) Münze Österreich AG
- AbsSynthe has participated in the second SyntComp which took place in 2015, this time co-located with CAV'15. AbsSynthe placed first in the sequential synthesis track once more. A report on the results of the competition can be fetched here and the new (native) version of AbsSynthe is available here.
- ERC Meeting @ Jerusalem, Israel [May 9-10, 2013]
- ERC Meeting @ IST Austria, Austria [March 12-13, 2015]