29 octobre 2009
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.
Slides
