Français Anglais
Accueil Annuaire Plan du site
Research results
Contract / grant for group Verification of Algorithms, Languages and Systems
VERASCO

ANR
Jan 2012 - Dec 2015

Group : Verification of Algorithms, Languages and Systems
Principal investigator : MELQUIOND Guillaume

Administrator : 
Affiliation : INRIA

VERASCO

The main goal of the project is to investigate the formal verification of static analyzers and of compilers, two families of tools that play a crucial role in the development and validation of critical embedded software. More precisely, the project aims at developing a generic static analyzer based on abstract interpretation for the C language, along with a number of advanced abstract domains and domain combination operators, and prove the soundness of this analyzer using the Coq proof assistant. Likewise, it will keep working on the CompCert C formally-verified compiler, the first realistic C compiler that has been mechanically proved to be free of miscompilation, and carry it to the point where it could be used in the critical software industry.

Research activities
  Formalisation and Proof of Numerical Programs
  Formalisation of (Specification and Programming) Languages in Proof Assistants
  Deductive Verification of Programs

Participants
MARCHÉ Claude
BOLDO Sylvie
MELQUIOND Guillaume


More information : http://verasco.imag.fr/
Contracts & grants
° VOCAL
VOCAL
ANR

° PARDI
PARDI
ANR

° DATACERT
DATACERT
ANR