Ressource pédagogique :  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 erre...
cours / présentation - Date de création : 08-10-2009
Auteur(s) : Xavier Leroy
Partagez !

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

Informations pratiques sur cette ressource

Français
Type pédagogique : cours / présentation
Niveau : enseignement supérieur, licence
Langue de l'apprenant : Français
Contenu : image en mouvement
Public(s) cible(s) : apprenant, enseignant
Document : Document HTML, Document PDF
Age attendu de l'utilisateur : 18 +
Difficulté : moyen
Taille : 4 Ko
Droits : pas libre de droits, gratuit
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)

Description de la ressource pédagogique

Description (résumé)

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.

  • Granularité : leçon
  • Structure : atomique

"Domaine(s)" et indice(s) Dewey

  • program verification (005.14)

Thème(s)

Informations pédagogiques

  • 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
  • Activité induite : s'informer, apprendre

Intervenants, édition et diffusion

Intervenants

Créateur(s) de la métadonnée : Marie-Hélène Comte;Marie-Hélène

Editeur(s)

Diffusion

Partagez !

AUTEUR(S)

  • Xavier Leroy
    INRIA - Centre de Recherche Paris - Rocquencourt

ÉDITION

Institut National de Recherche en Informatique et en Automatique

EN SAVOIR PLUS

  • Identifiant de la fiche
    http://ori.unit-c.fr/uid/unit-ori-wf-1-3521
  • Identifiant
    unit-ori-wf-1-3521
  • Statut de la fiche
    final
  • Schéma de la métadonnée
  • Entrepôt d'origine
    UNIT
  • Date de publication
    11-12-2009