Readable semi-automatic formal proofs of Depth-First Search in graphs using Why3

Ran Chen 1 Jean-Jacques Levy 2
2 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
Abstract : Quite often formal proofs are not published in conferences or journal articles, because formal proofs are usually too long. A typical article states the ability of having implemented a formal proof, but the proof itself is often sketched in terms of a natural language. At best, some formal lemmas and definitions are stated. Can we do better ? We try here to publish the details of a formal proof of the white-paths theorem about depth-first search in graphs. We use Why3 as the proving platform, because Why3 uses first-order logic augmented with inductive definitions of predicates and because Why3 makes possible to delegate bits of proofs to on-the-shelf automatic provers at same time as Why3 provides interfaces with interactive proof checkers such that Coq, PVS or Isabelle. Algorithms on graphs are also a good testbed since graphs are combinatorial structures whose algebraic properties are not fully obvious. Depth-first search may look over-simple, but it is the first step of the construction of a library of readable formal proofs for more complex algorithms on graphs with more realistic data structures.
Type de document :
Pré-publication, Document de travail
2015
Liste complète des métadonnées

Littérature citée [21 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01253136
Contributeur : Jean-Jacques Levy <>
Soumis le : vendredi 8 janvier 2016 - 16:45:41
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : jeudi 10 novembre 2016 - 22:37:01

Fichier

15dfswhy3.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01253136, version 1

Collections

INRIA | PPS | USPC

Citation

Ran Chen, Jean-Jacques Levy. Readable semi-automatic formal proofs of Depth-First Search in graphs using Why3. 2015. 〈hal-01253136〉

Partager

Métriques

Consultations de la notice

135

Téléchargements de fichiers

75