Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle

Ran Chen 1 Cyril Cohen 2 Jean-Jacques Levy 3 Stephan Merz 4 Laurent Thery 2
1 Institute of Software Chinese Academy of Sciences [Beijing]
2 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
3 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
4 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : Comparing provers on a formalization of the same problem is always a valuable exercise. In this paper, we present the formal proof of correctness of a non-trivial algorithm from graph theory that was carried out in three proof assistants: Why3, Coq, and Isabelle.
Keywords : Program verification Mathematical logic Formal proof Graph algorithm
Type de document :
Pré-publication, Document de travail
2018
Liste complète des métadonnées
https://hal.inria.fr/hal-01906155
Contributeur : Stephan Merz <>
Soumis le : vendredi 26 octobre 2018 - 14:43:12
Dernière modification le : vendredi 4 janvier 2019 - 17:33:38
Document(s) archivé(s) le : dimanche 27 janvier 2019 - 14:44:09

Fichiers

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

Identifiants

  • HAL Id : hal-01906155, version 1
  • ARXIV : 1810.11979

Collections

INRIA-ROCQ | UNIV-LORRAINE | LORIA | LORIA-FM | INRIA | UNIV-COTEDAZUR | USPC

Citation

Ran Chen, Cyril Cohen, Jean-Jacques Levy, Stephan Merz, Laurent Thery. Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle. 2018. 〈hal-01906155〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

48

Téléchargements de fichiers

49

Contact


archive-ouverte@inria.fr