URI http://ori.unit-c.fr/uid/unit-ori-wf-1-3521 Comment faire confiance à un compilateur ? (série : Colloquium Jacques Morgenstern) fre 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. compilateur logiciel critique programmation fonctionnelle vérification de programme vérification formelle preuve formelle fuscia conference stic recherche LOMv1.0 atomic LOMv1.0 2 LOMv1.0 image en mouvement LOMv1.0 final LOMv1.0 author BEGIN:VCARD VERSION:3.0 N:Leroy;Xavier;;; FN:Xavier Leroy EMAIL;TYPE=INTERNET:Xavier.Leroy@inria.fr ORG:INRIA - Centre de Recherche Paris - Rocquencourt END:VCARD 2009-10-08 LOMv1.0 publisher BEGIN:VCARD VERSION:3.0 N:Institut National de Recherche en Informatique et en Automatique;;;; FN:Institut National de Recherche en Informatique et en Automatique EMAIL;TYPE=INTERNET: ORG:INRIA END:VCARD 2009-12-11 URI http://ori.unit-c.fr/uid/unit-ori-wf-1-3522 LOMv1.0 creator BEGIN:VCARD VERSION:3.0 N:Comte;Marie-Hélène;Marie-Hélène;;; FN:Marie-Hélène Comte;Marie-Hélène EMAIL;TYPE=INTERNET:marie-Hélène.comte@sophia.inria.fr ORG:Inria, Institut National de recherche en Informatique et Automatique END:VCARD 2009-11-25 LOMv1.0 LOMFRv1.0 SupLOMFRv1.0 fre text/html application/pdf 4096 http://iww.inria.fr/colloquium/fr/xavier-leroy-comment-faire-confiance-a-un-compilateur/ LOMv1.0 lecture LOMv1.0 learner LOMv1.0 teacher LOMv1.0 higher education LOMFRv1.0 licence 18 + LOMv1.0 medium - 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 LOMFRv1.0 s'informer fre LOMFRv1.0 apprendre LOMv1.0 no LOMv1.0 yes Document libre, dans le cadre de la licence Creative Commons (http://creativecommons.org/licenses/by-nd/2.0/fr/), citation de l'auteur obligatoire et interdiction de désassembler (paternité, pas de modification) LOMv1.0 ispartof URI http://ori.unit-c.fr/uid/unit-ori-wf-1-3045 Colloquium Jacques Morgenstern LOMv1.0 discipline Classification UNIT 1307 Systèmes d'exploitation, interpréteurs, compilateurs Classification UNIT 1806 Qualité, Fiabilité, Sécurité LOMv1.0 discipline CDD 22e éd. 005.4 compilers computer programs CDD 22e éd. 005.14 program verification