Double WP : Vers une preuve automatique d'un compilateur

Martin Clochard 1, 2 Léon Gondelman 1, 2
1 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Résumé : Nous présentons une expérience qui vise à certifier un compilateur de manière la plus automatique possible. Nous avons mené cette expérience en utilisant l'environnement de preuve de programme Why3, ce qui nous permet de décharger les obligations de preuve à l'aide de prouveurs, notamment automatiques. Nous avons étudié deux approches différentes. La première, une approche directe, s'est montrée peu satisfaisante car très manuelle. Si l'on voit la preuve d'un compilateur comme la vérification que le code généré satisfait une spécification (dérivée du code source), on peut ramener la correction du compilateur à la correction du code qu'il produit. Notre deuxième approche consiste donc à exploiter des méthodes de preuve de programmes, proches de celles employées par Why3 lui-même, au niveau du code généré. Une telle méthode rend la preuve du compilateur quasi-automatique.
Type de document :
Communication dans un congrès
Journées Francophones des Langages Applicatifs, Jan 2015, Val d'Ajol, France. 2015, 〈http://jfla.inria.fr/2015/〉
Liste complète des métadonnées

Littérature citée [9 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01094488
Contributeur : Martin Clochard <>
Soumis le : vendredi 12 décembre 2014 - 13:41:56
Dernière modification le : vendredi 17 février 2017 - 16:10:49
Document(s) archivé(s) le : samedi 15 avril 2017 - 08:05:26

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01094488, version 1

Citation

Martin Clochard, Léon Gondelman. Double WP : Vers une preuve automatique d'un compilateur. Journées Francophones des Langages Applicatifs, Jan 2015, Val d'Ajol, France. 2015, 〈http://jfla.inria.fr/2015/〉. 〈hal-01094488〉

Partager

Métriques

Consultations de
la notice

426

Téléchargements du document

221