salle A. Turing CE4
11 mai 2012 - 10h00
Démonstration automatique : techniques, outils et certification.
par Xavier Urbain de ENSIIE
Résumé : Notre objectif est de permettre la vérification de programme à l'aide de méthodes fondées sur la preuve et aussi automatisées que possible. Je me concentrerai sur la preuve d'une propriété : la *terminaison*, dans des formalismes à base de récriture.
J'esquisserai tout d'abord un panel de techniques pour la preuve de terminaison, adaptées à différentes extensions qui, de proche en proche, mènent de la récriture du premier ordre (non sortée, en théorie libre...) au niveau de langages de programmation courants.
Ces techniques sont conçues pour établir *automatiquement* la propriété recherchée ; elles sont implantées dans un certain nombre d'outils (prouveurs) auxquels l'utilisateur doit faire confiance. Cependant, dans les faits, tous ces outils se sont un jour ou l'autre montrés défaillants, rendant délicate leur utilisation dans des domaines où le doute n'est pas permis (vérification de programmes critiques, etc.).
J'exposerai alors une approche, à base de génération et d'analyse de traces de preuve, qui permet de *certifier*, par exemple dans l'assistant à la preuve Coq, que les résultats des prouveurs sont corrects. Cette approche concourt ainsi à davantage d'automatisation, notamment en autorisant la délégation de la découverte de preuve à des outils externes à Coq.
Je conclurai sur les perspectives offertes par la maturité de ces techniques et approches, notamment dans le contexte de l'algorithmique distribuée.
