Skip to Main content Skip to Navigation
Conference papers

Des transformations logiques passent leur certicat

Résumé : Dans un contexte de vérification formelle de programmes, utilisant des démonstrateurs automatiques, la base de confiance des environnements de vérification est typiquement très large. Ainsi, un outil de vérification de programmes tel que Why3 comporte de nombreuses procédures complexes : génération de conditions de vérification, transformations logiques de tâches de preuve et interactions avec des démonstrateurs externes. En ne considérant que les transformations logiques dans Why3, leur implantation comporte déjà plus de 17000 lignes de code OCaml. Afin d'augmenter notre confiance dans la correction d'un tel outil de vérification, nous proposons un mécanisme de transformations certifiantes, produisant des certificats pouvant être validés par un outil externe, selon l'approche sceptique. Nous présentons ce mécanisme de génération de certificats et explorons deux méthodes pour les valider : une fondée sur un vérificateur dédié développé en OCaml, l'autre reposant sur le vérificateur de preuves universel Dedukti. Une spécificité de nos certificats est d'être « à petits grains » et composables, ce qui rend notre approche incrémentale, permettant d'ajouter graduellement de nouvelles transformations certifiantes.
Document type :
Conference papers
Complete list of metadatas

Cited literature [15 references]  Display  Hide  Download

https://hal.inria.fr/hal-02384946
Contributor : Quentin Garchery <>
Submitted on : Friday, December 6, 2019 - 3:10:23 PM
Last modification on : Friday, October 9, 2020 - 10:03:27 AM
Long-term archiving on: : Saturday, March 7, 2020 - 5:23:56 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02384946, version 2

Citation

Quentin Garchery, Chantal Keller, Claude Marché, Andrei Paskevich. Des transformations logiques passent leur certicat. JFLA 2020 - Journées Francophones des Langages Applicatifs, Jan 2020, Gruissan, France. ⟨hal-02384946v2⟩

Share

Metrics

Record views

167

Files downloads

501