English

Projet A3PAT

ASSISTER  AUTOMATIQUEMENT LES ASSISTANTS DE
PREUVE AVEC DES TRACES

Take nothing on its looks; take everything on evidence. There's no better rule.
(Jaggers) C. Dickens Great Expectations.



Les assistants de preuve sceptiques comme Coq ou Isabelle bénéficient d'un noyau de vérification très sûr. Pour Coq, par exemple, le typage d'un terme de preuve permet de vérifier qu'une preuve est correcte. Les environnements de programmation certifiée qui les utilisent comme fondation trouvent ainsi une garantie de correction du code produit.

Ces assistants souffrent toutefois d'un manque d'automatisation de la recherche de preuve.

L'automatisation est difficile à obtenir dans ce cadre : il ne suffit pas d'obtenir le résultat de procédures de décision automatiques externes, aussi performantes soient-elles. L'assistant refusera en effet de considérer une propriété s'il n'en connait pas de preuve. Celle-ci doit pouvoir être vérifiée par le noyau de certification ; on doit fournir un certificat compréhensible par ce dernier de la preuve de la propriété.

On observe ainsi une séparation entre les assistants qui offrent des garanties formelles de confiance et les outils automatiques performants dont on doit croire les résultats.

Objectif

Le projet A3PAT souhaite répondre au besoin important de délégation de la preuve de certaines propriétés dans le cadre des techniques liées à la récriture, notamment en définissant des moyens génériques d'exprimer des certificats à la taille raisonnable de propriétés complexes.

Les verrous scientifiques sont à la fois d'ordre théorique et pratique :

Mise en œuvre

À terme, une mise en œuvre des avancées proposées prendra forme à travers le développement d'une nouvelle version de l'outil CiME que nous souhaitons rendre capable de produire des traces vérifiables mécaniquement, par Coq par exemple, des manipulations effectuées et des preuves trouvées.