Français Anglais
Accueil Annuaire Plan du site
Production scientifique
Contrat de l'équipe Vérification d'Algorithmes, Langages et Systèmes
VERASCO

ANR
Janv. 2012 - Déc. 2015

Equipe : Vérification d'Algorithmes, Langages et Systèmes
Responsable : MELQUIOND Guillaume

Gestionnaire : 
Organisme gérant : INRIA

ANR 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.

Activités de recherche
  Formalisation et preuves de programmes numériques
  Formalisation de langages (de spécification et de programmation) dans les assistants de preuve
  Vérification déductive de programmes

Membres LRI
MARCHÉ Claude
BOLDO Sylvie
MELQUIOND Guillaume


Pour en savoir plus : http://verasco.imag.fr/
Contrats
° SOPRANO
SOPRANO
ANR

° ORACLE AMERICA INC
ORACLE AMERICA INC

° VOCAL
VOCAL
ANR

° PARDI
PARDI
ANR

° LCHIP
LCHIP