Les assistants de preuve comme Coq sont devenus des instruments de plus en plus utilisés dans les processus de vérification. Ils fournissent un moyen mécanique de vérifier un résultat. La vérification mécanique est d'autant plus intéressante si les spécifications qui sont entrées dans l'assistant sont proches de la présentation usuelle du problème. Dans ce cas on a prouvé formellement que la propriété découle de l'énoncé du problème.
Pour les preuves la situation n'est pas aussi satisfaisante. Chaque système de preuve a son langage propre. De plus ce langage est habituellement plus procédural que déclaratif. Les preuves mécaniques ressemblent donc plus à des programmes qui expliquent comment construire une preuve qu'à des preuve usuelles. Le but de ce stage est de proposer des solutions pour changer cet état de fait. L'approche proposée est de considérer la preuve comme un acteur de la vérification. Il ne s'agit plus seulement de prouver qu'une propriété découle des spécifications mais que l'énoncé découle des spécifications par une preuve donnée. Ainsi les preuves deviennent en un certain sens certifiées. Pour la réalisation on s'inspirera de ce qui a été fait dans le domaine vérification de programme, où l'on se permet d'annoter des programmes avec des assertions pour en faciliter sa vérification. Il s'agira donc de définir un format de preuves annotées et de construire les outils nécessaires pour analyser de telles preuves.
E-mail : Laurent.Thery@sophia.inria.fr
[1] G. Huet, G. Kahn, C. Paulin-Mohring, The Coq Proof Assistant : A Tutorial : Version 6.1, Rapport Technique INRIA 0204, août 1997.
[2] John Harrison, Proof Style, rapport technique, cambridge, 1997.
[3]Yann Coscoy, Gilles Kahn, and Laurent Théry, ``Extracting Text from Proof'', INRIA Rapport de recherche no. 2459, January 95.