Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle - Archive ouverte HAL Access content directly
Preprints, Working Papers, ... Year :

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

(1) , (2) , (3) , (4, 5) , (2)
1
2
3
4
5

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.
Fichier principal
Vignette du fichier
paper.pdf (409.99 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

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

Identifiers

Cite

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⟩
194 View
227 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More