Comment faire confiance à un compilateur ? (série : Colloquium Jacques Morgenstern)

Les outils de vérification formelle de programmes (analyseurs statiques,prouveurs de programmes,model-checkers) ont fait des progrès remarquables ces dernières années et commencent à percer dans le monde du logiciel critique. Cependant,ces outils ne vérifient que des programmes source: des erreurs dans les compilateurs qui les transforment en code machine exécutable ou dans les processeurs qui les exécutent peuvent toujours invalider les garanties obtenues par vérification du source. Je présenterai un projet en cours,appelé Compcert,qui vise à éliminer totalement cette incertitude dans le cas des compilateurs. Il s'agit d'un compilateur réaliste pour le sous-ensemble embarqué critique du langage C qui s'accompagne d'une preuve mathématique de préservation sémantique,montrant que le compilateur ne va jamais introduire d'erreurs dans le programme qu'il compile. Nous utilisons l'assistant de preuve Coq non seulement pour conduire cette preuve,mais aussi comme langage de programmation pour écrire le compilateur lui-même. Je terminerai par quelques perspectives plus générales sur l'avenir des langages et outils de programmation vus sous l'angle de la vérification formelle de programmes.

Mots-clés : compilateur,logiciel critique,programmation fonctionnelle,vérification de programme,vérification formelle,preuve formelle,fuscia,conference,stic,recherche
Type de document : image en mouvement
Type de ressource : lecture
Niveau : higher education,licence
Publics visés : learner,teacher
Activité induite : s'informer,apprendre
Proposition d'utilisation : - pour illustrer  l'utilisation des méthodes formelles dans  la vérification de programmes  lors d' un cours sur la programmation fonctionnelle ou sur  les compilateurs. - pour comprendre les problématiques de l'industrie du logiciel critique
Auteurs ou éditeurs : Xavier Leroy,Institut National de Recherche en Informatique et en Automatique