Démonstration automatique en Coq

Quentin Garchery (1, 2, 3)

1 UPD7 - Université Paris Diderot - Paris 7
2 LRI - Laboratoire de Recherche en Informatique
3 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations

Les méthodes formelles rassemblent différents logiciels formels qui permettent de formuler des propriétés mathématiques puis de les vérifier. La validité du résultat ne dépend alors que de ce logiciel de vérification. On considère deux familles de logiciels formels : les assistants de preuve et les prouveurs automatiques. D'un côté, les assistants de preuve sont expressifs mais demandent un effort de certification de la part de l'utilisateur. D'un autre côté, les prouveurs automatiques se chargent de fournir la preuve de la propriété énoncée ce qui n'est possible que lorsque la logique utilisée est plus limitée. Les interfaces entre un assistant de preuve et différents prouveurs automatiques telles que SMTCoq permettent d'obtenir les avantages de ces deux familles en améliorant l'automatisation de l'assistant de preuve considéré. Cette amélioration de l'automatisation est d'autant plus pertinente que le fragment de la logique des prouveurs automatiques pris en compte par l'interface est important. Dans ce rapport, on se propose d'augmenter le fragment pris en compte par SMTCoq en permettant la preuve automatique de propriétés qui ont pour hypothèses des lemmes en forme prénexe.

Mots clés: Master's thesis

Domaines: Théorie et langage formel [cs.FL]

Quentin Garchery. Démonstration automatique en Coq. [Travaux universitaires] Paris Diderot; Laboratoire de recherche en informatique (LRI) UMR CNRS 8623, Université Paris-Sud. 2018. ⟨hal-01874777⟩