Vérification formelle d'un compilateur réaliste du langage C

Les compilateurs sont des logiciels fort complexes qui parfois contiennent des erreurs entraînant la production de code exécutable faux à partir d'un programme source correct. L'existence de tels bugs introduits par le compilateur affaiblit les garanties que l'on peut obtenir par l'application de méthodes formelles au niveau du programme source.

Cet exposé présente le compilateur CompCert, un compilateur réaliste, modérément optimisant, produisant de l'assembleur PowerPC à partir d'un large sous-ensemble du langage C. CompCert a été développé et prouvé correct à l'aide de l'assistant à la preuve Coq. La preuve de correction établit que le code PowerPC engendré se comporte exactement comme prescrit par la sémantique du source C, éradiquant ainsi toute possibilité de bugs introduits par le compilateur et établissant un niveau de confiance sans précédent envers ce compilateur.

Travail commun avec Xavier Leroy (INRIA Paris-Rocquencourt)