Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Pré-Publication, Document De Travail Année : 2018

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

Résumé

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

Dates et versions

hal-01906155 , version 1 (26-10-2018)

Identifiants

Citer

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⟩
242 Consultations
288 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More