Double WP : Vers une preuve automatique d'un compilateur

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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [9 references]  Display  Hide  Download

https://hal.inria.fr/hal-01094488
Contributor : Martin Clochard <>
Submitted on : Friday, December 12, 2014 - 1:41:56 PM
Last modification on : Friday, October 4, 2019 - 1:47:31 AM
Long-term archiving on : Saturday, April 15, 2017 - 8:05:26 AM

File

main.pdf
Files produced by the author(s)

Identifiers

  • 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. ⟨hal-01094488⟩

Share

Metrics

Record views

577

Files downloads

387