INVEST
inVEST: Foundations for a Shift from Verification to Synthesis
| Coordinatore | UNIVERSITE LIBRE DE BRUXELLES
Spiacenti, non ci sono informazioni su questo coordinatore. Contattare Fabio per maggiori infomrazioni, grazie. |
| Nazionalità Coordinatore | Belgium [BE] |
| Totale costo | 1˙415˙255 € |
| EC contributo | 1˙415˙255 € |
| Programma | FP7-IDEAS-ERC
Specific programme: "Ideas" implementing the Seventh Framework Programme of the European Community for research, technological development and demonstration activities (2007 to 2013) |
| Code Call | ERC-2011-StG_20101014 |
| Funding Scheme | ERC-SG |
| Anno di inizio | 2012 |
| Periodo (anno-mese-giorno) | 2012-01-01 - 2016-12-31 |
Partecipanti
| # | ||||
|---|---|---|---|---|
| 1 |
UNIVERSITE LIBRE DE BRUXELLES
Organization address
address: Avenue Franklin Roosevelt 50 contact info |
BE (BRUXELLES) | hostInstitution | 1˙415˙255.40 |
| 2 |
UNIVERSITE LIBRE DE BRUXELLES
Organization address
address: Avenue Franklin Roosevelt 50 contact info |
BE (BRUXELLES) | hostInstitution | 1˙415˙255.40 |
Mappa
Word cloud
Esplora la "nuvola delle parole (Word Cloud) per avere un'idea di massima del progetto.
Obiettivo del progetto (Objective)
'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 mathematically deeper, game-theoretic framework. Our work will be of fundamental nature but will also aim at the development of algorithms and 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.'