Proposition de stage de Master 2ème année
Coopération d'outils de preuve interactifs et automatiques

Laboratoire : LRI -- CNRS 8623, Université Paris Sud, 91405 ORSAY Cedex
Directeur de laboratoire : M. Beaudouin-Lafon (mbl@lri.fr)
Équipe : Démonstration et Programmation (http://www.lri.fr/demons/)
Directeur de stage : J.-C. Filliâtre (filliatr@lri.fr)

Domaine.
Ce stage s'inscrit dans le contexte de la vérification formelle de programmes, c'est-à-dire la preuve assistée par ordinateur qu'un programme vérifie une spécification donnée. Dans l'équipe Démonstration et Programmation du LRI, nous développons des outils de vérification formelle de programmes Java et C.

Objectifs du stage.
Ces logiciels de preuve de programme reposent eux-même sur des outils d'assistance à la démonstration existants, certains étant interactifs (Coq, PVS, HOL Light, Mizar) et d'autres purement automatiques (Simplify, CVC Lite, haRVey). Pour l'instant ces outils ne collaborent pas, ils ne sont que des alternatives. L'objectif de ce stage est de permettre la collaboration entre ces divers outils de preuve.

Un premier objectif, modeste, consistera à interfacer l'assistant de preuve interactif Coq [1] avec les procédures de décision automatiques Simplify [2] et CVC Lite [3]. Plus précisément, il s'agira de pouvoir appeler ces procédures de décision à partir de Coq, en supposant leur résultat correct. On s'attachera à mettre en place une technologie aussi générique que possible, de manière à faciliter l'intégration d'autres procédures de décision.

Un second objectif, plus ambitieux, consistera à interpréter les traces de preuve fournies par CVC Lite pour les traduire en des preuves Coq. Ce travail pourra s'appuyer sur une expérience similaire menée dans l'assistant de preuve Isabelle [4].

Pré-requis :
Programmation, Logique. Cours concerné : 2-7.

References

[1]
L'assistant de preuve Coq. http://coq.inria.fr/
[2]
Simplify. http://research.compaq.com/SRC/esc/Simplify.html
[3]
CVC Lite http://verify.stanford.edu/CVCL/
[4]
Tom Harke. Toward a sound integration of Isabelle with combined decision procedures. http://www.cse.ogi.edu/~harke/RPE-paper.ps
This document was translated from LATEX by HEVEA.