Des transformations logiques passent leur certificat - INRIA - Institut National de Recherche en Informatique et en Automatique Accéder directement au contenu
Communication Dans Un Congrès Année : 2020

Des transformations logiques passent leur certificat

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.
Fichier principal
Vignette du fichier
main.pdf (643.96 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02384946 , version 1 (28-11-2019)
hal-02384946 , version 2 (06-12-2019)

Identifiants

  • HAL Id : hal-02384946 , version 2

Citer

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

Partager

Gmail Facebook X LinkedIn More