Le projet



Porteur :
Appel à projet :
Statut :
en cours
Groupes Thématiques :
Date de fin de projet :
Durée :
48 mois
Montant total :
4 399 K€
Montant aide :
996 K€
Axe :
Software engineering
Description :

In its quest for software perfection, the critical software industry has been progressively embracing the use of formal verification tools (static analyzers, program provers, model checkers) as a complement, or even as an alternative, to traditional software validation techniques based on testing and reviews. The usefulness of verification tools in the certification of critical software is, however, limited by the amount of trust one can have in their results. Two major risks exist: unsoundness of verification tools (failing to detect a misbehaving program) and miscompilation (post-verification introduction of bugs during the production of executable code). The Verasco project investigates a radical, mathematically-grounded solution to these issues: the formal verification of compilers and verification tools themselves.

Les membres

Membres impliqués dans le projet :