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

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

Mathematical logic Formal proof Graph algorithm Program verification

Domains

Computer Science [cs] Logic in Computer Science [cs.LO]

Fichier principal

paper.pdf (409.99 Ko)

Origin : Files produced by the author(s)

Stephan Merz : Connect in order to contact the contributor

https://hal.inria.fr/hal-01906155

Submitted on : Friday, October 26, 2018-2:43:12 PM

Last modification on : Tuesday, October 25, 2022-4:17:01 PM

Long-term archiving on: Sunday, January 27, 2019-2:44:09 PM

Dates and versions

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

Identifiers

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

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⟩

Export

BibTeX TEI Dublin Core DC Terms EndNote Datacite

Collections

UNIV-PARIS7 CNRS INRIA UNIV-LORRAINE INRIA2 LORIA LORIA-FM USPC UNIV-COTEDAZUR UNIV-PARIS UP-SCIENCES ANR IRIF

194 View

227 Download