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
° IUF
FABIO MARTIGNON
SUBVENTION

° DIGISCOPE UPS
INFRASTRUCTURE HAUTE PERFORMANCE POUR LA VISUALISATION INTERACTIVE ET COLLABORATIVE
ANR

° DIGISCOPE CNRS
INFRASTRUCTURE HAUTE PERFORMANCE POUR LA VISUALISATION INTERACTIVE ET COLLABORATIVE
ANR

° LCHIP
LCHIP

° DIGISCOPE INRIA
INFRASTRUCTURE HAUTE PERFORMANCE POUR LA VISUALISATION INTERACTIVE ET COLLABORATIVE
ANR