Les dépôts de projets se font directement sur le site de l'ANR à l'adresse suivante :
Appel à projets générique Edition 2016: http://www.agence-nationale-recherche.fr/AAPG2016


Merci de prendre connaissance du schéma général d'application de l'accord FRAE/ANR dans le dispositif d'appel à projets générique de l'ANR 2016

LES EXPERTS

Les Experts scientifiques et industriels sont des personnes « extérieures » à la Fondation.

EN SAVOIR +

ASCERT

Analyses Statiques CERTifiées

  Nous proposons d'étudier la certification formelle des analyses statiques en utilisant l'assistant de preuve Coq. Nous aborderons plusieurs techniques permettant de démontrer mécaniquement la validité sémantique du diagnostique d'un analyseur : programmation certifiée correcte de l'analyseur, certification d'un vérificateur de résultat et validation déductive des invariants générés par un analyseur. Nous étudierons plusieurs composants clés
de l'analyseur Astrée. Notre première tâche se consacrera à la certification des opérateurs de la bibliothèque de domaines abstraits Apron. Nous étudierons ensuite un interpréteur abstrait avant/arrière pour un langage impératif simple. Enfin nous relierons cet interpréteur à une des
sémantiques formelles de C, développés dans le projet CompCert. Tous ces objectifs ont pour ambition commune de pouvoir, au terme du projet, évaluer le coût d'une certification formelle d'un tel analyseur.

Partenaires :

Coordinateur INRIA
ENS

Coordinateur et contact :

PICHARDIE David
david.pichardie@irisa.fr

  • Durée : 36 mois
  • Date de démarrage : 01/04/2009
  • Projet : terminé

 

Fondation de Recherche pour l'Aéronautique et l'Espace
F.R.A.E. - 10 Avenue Edouard Belin - 31400 Toulouse
Tél. : 05 62 88 69 92 - Mail : contact@fnrae.org