Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

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

Ran Chen 1 Cyril Cohen 2 Jean-Jacques Levy 3 Stephan Merz 4, 5 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
UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique, IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale, Inria de Paris
4 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
5 MOSEL - Proof-oriented development of computer-based systems
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
Document type :
Preprints, Working Papers, ...
Complete list of metadata
https://hal.inria.fr/hal-01906155
Contributor : Stephan Merz Connect in order to contact the contributor
Submitted on : Friday, October 26, 2018 - 2:43:12 PM
Last modification on : Saturday, October 16, 2021 - 11:26:09 AM
Long-term archiving on: : Sunday, January 27, 2019 - 2:44:09 PM

Files

Vignette du document
paper.pdf
Files produced by the author(s)

Identifiers

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

Collections

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

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⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

304

Files downloads

245

 

Contact                    Legal Notice                    Personal Data