Ressource en auto-formation :  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 - Création : 08-10-2009
Par : Xavier Leroy
Partagez !

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

Informations pratiques sur cette ressource

Langue du document : Français
Type : cours / présentation
Niveau : enseignement supérieur, licence
Langues : Français
Contenu : vidéo
Public(s) cible(s) : apprenant, enseignant
Document : Document HTML, Document PDF
Age attendu : 18 +
Difficulté : moyen
Poids : 4 Ko
Droits d'auteur : 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 en auto-formation

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)

Domaine(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

Édition

  • Institut National de Recherche en Informatique et en Automatique

Diffusion

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

Partagez !

AUTEUR(S)

  • Xavier Leroy
    INRIA - Centre de Recherche Paris - Rocquencourt

DIFFUSION

Cette ressource en auto-formation vous est proposée par :
UNIT - accédez au site internet
Sur les réseaux sociaux :

É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 OAI-PMH
    oai:www.unit.eu:unit-ori-wf-1-3521
  • Statut de la fiche
    final
  • Schéma de la métadonnée
  • Entrepôt d'origine
    UNIT
  • Publication
    11-12-2009

Ressources en auto-formation sur les mêmes thèmes

Présentation de la ressource en auto-formation Preuves de programmes en coq cours / présentation, outil, exercice, liste de références
21/09/2012
Preuves de programmes en coq
Auteur(s) : Bertot Yves
Description : Le système Coq fournit un langage de programmation symbolique et un cadre logique pour raisonner sur les algorithmes décrits. Dans ce cours, nous décrivons les points clefs du langage de programmation, basé sur la programmation fonctionnelle, et du cadre logique de vérification, basé sur la logique ...
Présentation de la ressource en auto-formation Do general purpose languages have a future? cours / présentation
02/06/2009
Do general purpose languages have a future?
Auteur(s) : Stroustrup Bjarne
Description : As the computing world matures, the roles of computer professionals are becoming more specialized. In particular, a programmer can spend a whole career doing work in embedded systems or data analysis without a need to gain expertise in other fields. Would such programmers be best served by completely ...