Strongly Connected Components in graphs, formal proof of Tarjan1972 algorithm

Jean-Jacques Levy 1 Ran Chen 2, 3
1 PI.R2 - Design, study and implementation of languages for proofs and programs
Inria de Paris, CNRS - Centre National de la Recherche Scientifique, UPD7 - Université Paris Diderot - Paris 7, PPS - Preuves, Programmes et Systèmes
3 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
Résumé : Nous présentons une preuve formelle de l'algorithme de Tarjan (1972) pour trouver les composantes fortement connexes dans un graphe. Cet algorithme exécute une seule passe sur le graphe le parcourant en profondeur d'abord. Notre programme est ici écrit dans un style de programmation fonctionnelle dans le langage Why3-ML. La preuve utilise des lemmes et des assertions exprimés dans la logique de Why3. La majorité d'entre eux sont prouvés automatiquement à l'exception de 5 assertions ou lemmes prouvés manuellement en Coq. Une preuve d'une version impérative de ce programme ne figure pas dans ce travail, mais nous indiquons comment y parvenir par raffinements successifs. Un point important est que nos preuves sont intuitives, publiables et lisibles par un humain.
Type de document :
Document associé à des manifestations scientifiques
Groupe de travail LTP du GDR GPL , Nov 2016, Orsay, France. 2016
Liste complète des métadonnées

https://hal.inria.fr/hal-01422227
Contributeur : Jean-Jacques Levy <>
Soumis le : samedi 24 décembre 2016 - 10:59:18
Dernière modification le : jeudi 26 avril 2018 - 10:28:28
Document(s) archivé(s) le : samedi 25 mars 2017 - 12:30:20

Fichier

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

Identifiants

  • HAL Id : hal-01422227, version 1

Citation

Jean-Jacques Levy, Ran Chen. Strongly Connected Components in graphs, formal proof of Tarjan1972 algorithm. Groupe de travail LTP du GDR GPL , Nov 2016, Orsay, France. 2016. 〈hal-01422227〉

Partager

Métriques

Consultations de la notice

370

Téléchargements de fichiers

27