|
 
|
[Jac13] Automatisation des preuves pour la vérification des règles de l'Atelier B
Mémoire de Thèse : Soutenue le: 23 April 2013, pp. 190, pp.: Directeur: Dubois - Delahaye - BerkaniRapporteur 1: C. Kirchner
Rapporteur 2: S. Merz
Membre du jury: J.-L. Boulanger
Membre du jury: D. Doligez
Membre du jury: M.-L. Potet, : Automatisation des preuves pour la vérification des règles de l'Atelier B,
motcle:
Résumé:
Cette thèse porte sur la vérification des règles ajoutées de l'Atelier B en
utilisant une plate-forme appelée BCARe qui repose sur un plongement de la
théorie sous-jacente à la méthode B (théorie de B) dans l'assistant à la
preuve Coq. En particulier, nous proposons trois approches pour prouver la
validité d'une règle, ce qui revient à prouver une formule exprimée dans la
théorie de B. Ces trois approches ont été évaluées sur les règles de la
base de règles de SIEMENS IC-MOL. La première approche dite autarcique est
développée avec le langage de tactiques de Coq Ltac. Elle repose sur une
première étape qui consiste à déplier tous les opérateurs ensemblistes pour
obtenir une formule de la logique du premier ordre. Puis nous appliquons
une procédure de décision qui met en oeuvre une heuristique naïve en ce qui
concerne les instanciations. La deuxième approche, dite sceptique, utilise
le prouveur automatique de théorèmes Zenon après avoir effectué l'étape de
normalisation précédente. Nous vérifions ensuite les preuves trouvées par
Zenon dans le plongement profond de B en Coq. La troisième approche évite
l'étape de normalisation précédente grâce à une extension de Zenon
utilisant des règles d'inférence spécifiques à la théorie de B. Ces règles
sont obtenues grâce à la technique de superdéduction. Cette dernière
approche est généralisée en une extension de Zenon à toute théorie grâce Ã
un calcul dynamique des règles de superdéduction. Ce nouvel outil, appelé
Super Zenon, peut par exemple prouver des problèmes issus de la
bibliothèque de problèmes TPTP.
Equipe:
sys
BibTeX
| @phdthesis { | |||
| Jac13, | |||
| title | = | "{Automatisation des preuves pour la vérification des règles de l'Atelier B}", | |
| author | = | "M. Jacquel", | |
| year | = | 2013, | |
| pages | = | "190", | |
| address | = | "{CEDRIC Laboratory, Paris, France}", | |
| note | = | "{ Directeur: Dubois - Delahaye - Berkani Rapporteur 1: C. Kirchner Rapporteur 2: S. Merz Membre du jury: J.-L. Boulanger Membre du jury: D. Doligez Membre du jury: M.-L. Potet}", | |
| } |
