Automatisation de la certification formelle de systèmes critiques par instrumentation d'interpréteurs abstraits

摘要: Les travaux menes dans cette these portent sur la certification de programmes. certificats etablissent validite des proprietes semantiques Ils sont produits sous forme preuves deductives verifiables par machine. Le defi releve est d'automatiser construction correction calculees analyseurs statiques programmes qui s'appuient theorie l'interpretation abstraite. Nous proposons une methode d'instrumentation anaJyseurs afin leur faire generer automatiquement un certificat pour chaque propriete semantique calculee. L'instrumentation consiste a associer certaines fonctions d'un analyseur statique patrons preuve. De tels instrumentes ne pas autant certifies puisque toutes leurs entrees possibles n'est garantie. Cette approche permet certifier avec tres haut-niveau confiance les resultats d'outils existants, meme l'etat prototypes. Pour que l'instrumentation soit applicable en pratique, nous avons cherche limiter le nombre instrumenter. degage ensemble restreint fonctions, commun tout analyseur, instrumenter qu'un existant devienne outil certification. applique technique manipulant tableaux et s'appuyant domaines abstraits non triviaux. Cet calcule contenu manipules grâce notre instrumentation il genere desormais Coq.