logo ANR Le projet ASCERT est financé par la Fondation de Recherche pour l'Aéronautique et l'Espace.

L'analyse statique par interprétation abstraite a démontré, au cours des dernières années, sa capacité à garantir l'absence de larges classes d'erreurs de programmation dans les logiciels critiques de grandes tailles. Cependant, les analyseurs statiques sont des programmes complexes sujets à des erreurs de programmation et on peut s'interroger sur la validité de leurs résultats. Cela conduit naturellement à proposer l'utilisation de méthodes formelles, notamment la preuve de programmes, pour certifier la correction d'analyseurs statiques par rapport à la théorie de l'interprétation abstraite qui en est le fondement et obtenir des garanties fortes sur la confiance que l'on peut accorder. Au travers du projet ASCERT, une étude de la certification formelle des analyses statiques sera réalisée en utilisant l'assistant de preuve Coq.

Plusieurs techniques permettant de démontrer mécaniquement la validité sémantique du diagnostique d'un analyseur seront abordées : 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. ASCERT étudiera la certification de plusieurs techniques de pointe en interprétation abstraite : quelques-uns des domaines abstraits relationnels de la bibliothèque Apron pour l'arithmétique bornée et flottante, un interpréteur abstrait avant/arrière pour un langage impératif simple et son extension à une des sémantiques formelles de C du projet CompCert.