Double WP : Vers une preuve automatique d'un compilateur - Archive ouverte HAL Access content directly
Conference Papers Year : 2015

Double WP : Vers une preuve automatique d'un compilateur

(1, 2) , (1, 2)
1
2

Abstract

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.
Fichier principal
Vignette du fichier
main.pdf (318.46 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01094488 , version 1 (12-12-2014)

Identifiers

  • HAL Id : hal-01094488 , version 1

Cite

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⟩
441 View
243 Download

Share

Gmail Facebook Twitter LinkedIn More