Formal proofs of two algorithms for strongly connected components in graphs

Ran Chen 1, 2 Jean-Jacques Levy 3
2 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
3 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique, Inria de Paris
Abstract : We present formal proofs for the two classical Tarjan-1972 and Kosaraju-1978 algorithms for finding strongly connected components in directed graphs. We describe the two algorithms in a functional programming style with abstract values for vertices in graphs, with functions between vertices and their successors, and with data types such that lists (for representing immutable stacks) and sets. We use the Why3 system and the Why3-logic to express these proofs and fully check them by computer. The Why3-logic is a simple multi-sorted first-order logic augmented by inductively defined predicates. Furthermore it provides useful libraries for lists and sets. The Why3 system allows description of programs in a Why3-ML programming language (a first-order programming language with ML syntax) and provides interfaces to various state-of-the-art automatic provers and to manual interactive proof-checkers (we use mainly Coq). One important point of our article is that our proofs are intuitive and human readable.
Type de document :
Pré-publication, Document de travail
2016
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01422216
Contributeur : Jean-Jacques Levy <>
Soumis le : samedi 24 décembre 2016 - 10:07:39
Dernière modification le : jeudi 26 avril 2018 - 10:28:45
Document(s) archivé(s) le : lundi 20 mars 2017 - 20:37:37

Fichier

16sccs.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01422216, version 1

Citation

Ran Chen, Jean-Jacques Levy. Formal proofs of two algorithms for strongly connected components in graphs. 2016. 〈hal-01422216〉

Partager

Métriques

Consultations de la notice

289

Téléchargements de fichiers

56