ASCERT

  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.