inVEST - Foundations
for a Shift from Verification to Synthesis
Summary
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.
Budget:
1.415.255€.
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
Potential candidates can directly
contact the PI of the project at the following email address: jraskin
[at] ulb [dot] ac [dot] be.a