Double WP : Vers une preuve automatique d'un compilateur

Martin Clochard (1, 2) , Léon Gondelman (1, 2)

1 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations
2 LRI - Laboratoire de Recherche en Informatique

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.

Domaines: Logique en informatique [cs.LO]

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⟩