Vérification formelle d'un compilateur réaliste du langage C
le 6 avril 2010
de 15h30 à 17h00ENS Rennes Salle du conseil
Intervention de Sandrine Blazy, professeure à l'université de Rennes 1 (séminaire du département Informatique et télécommunications).
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)
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)
- Thématique(s)
- Formation, Recherche - Valorisation
- Contact
- Claude Jard
Mise à jour le 9 septembre 2019
À télécharger
- transparents PDF, 1 Mo