Evènement pour le groupe Graphes et Logique


Date 2011-03-21  07:00-07:00
TitreDémonstration automatique : techniques, outils et certification. 
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. 
Lieusalle 76 
OrateurXavier Urbain 
Emailxavier.urbain@ensiie.fr 
UrlENSIIE, INRIA Saclay Ile de France, LRI 



Aucun document lié à cet événement.

Retour
Retour à l'index