Raisonnement fiable pour la Méthode B
Trustworthy Reasoning for the B Method
Jury
Directeur de these_MERZ_Stephan_Centre Inria de l'Université de Lorraine
Rapporteur_FILLIâTRE_Jean-Christophe_LMF, Paris Saclay
Rapporteur_LEUSCHEL_Michael_Heinrich-Heine-Universität Düsseldorf
Examinateur_KOVáCS_Laura_Faculty of Informatics Vienna University of Technology (TU Wien)
Examinateur_GOAOC_Xavier_Université de Lorraine
CoDirecteur de these_TOURRET_Sophie_Centre Inria de l'Université de Lorraine
école doctorale
IAEM - INFORMATIQUE - AUTOMATIQUE - ELECTRONIQUE - ELECTROTECHNIQUE - MATHEMATIQUES
Laboratoire
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Mention de diplôme
Informatique
Salle A008
LORIA, 615 Rue du Jardin Botanique, 54600 Villers-lès-Nancy
Mots clés
Preuve de théorèmes,Logique,Méthodes formelles,Lean,Encodage,Raisonnement automatisé,
Résumé de la thèse
La méthode B produit des obligations de preuve dont l'acquittement est essentiel pour établir la correction des systèmes développés. Étendre son environnement de preuve à des outils de raisonnement modernes soulève deux difficultés complémentaires : traduire fidèlement le langage ensembliste de B vers les langages typés des solveurs automatiques, et offrir un cadre interactif expressif pour les obligations que l'automatisation ne résout pas.
Keywords
Theorem proving,Logic,Formal methods,Lean,Encoding,Automated reasoning,
Abstract
The B method produces proof obligations whose discharge is essential to establishing the correctness of developed systems. Extending its proving environment with modern reasoners raises two complementary challenges: translating B's set-theoretic language faithfully into the typed languages of automated solvers, and providing an expressive interactive setting for obligations that automation does not solve.
