Abstract FR:

Nous nous intéressons dans cette thèse à la preuve formelle de correction des analyses statiques. Nous nous basons sur la théorie de l'interprétation abstraite qui présente une analyse statique comme une sémantique approchée d'un programme. Nous utilisons l'assistant de preuve Coq qui permet d'extraire le contenu calculatoire d'une preuve constructive. L'implémentation Caml certifiée d'une analyse peut ainsi être extraite de la preuve d'existence, pour tout programme, d'une approximation correcte de la sémantique concrète de ce programme. Nous présentons un cadre théorique fondé sur l'interprétation abstraite et permettant le développement formel d'une large gamme d'analyses statiques. Une bibliothèque Coq de construction modulaire de treillis est ensuite proposée. Des preuves complexes de terminaison de calcul itératif de point fixe peuvent ainsi Ítre construites par simple composition de foncteurs. Plusieurs cas d'études pour l'analyse de programme en bytecode Java sont présentés.