Skip to Main content Skip to Navigation
Conference papers

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

Ran Chen 1 Cyril Cohen 2 Jean-Jacques Levy 3 Stephan Merz 4, 5 Laurent Théry 6, 7
3 PI.R2 - Design, study and implementation of languages for proofs and programs
Inria de Paris, CNRS - Centre National de la Recherche Scientifique, IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale, UPD7 - Université Paris Diderot - Paris 7
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
6 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
7 STAMP - Sûreté du logiciel et Preuves Mathématiques Formalisées
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : Comparing provers on a formalization of the same problem is always a valuable exercise. In thispaper, we present the formal proof of correctness of a non-trivial algorithm from graph theory thatwas carried out in three proof assistants: Why3,Coq, and Isabelle.
Document type :
Conference papers
Complete list of metadata

Cited literature [36 references]  Display  Hide  Download

https://hal.inria.fr/hal-02303987
Contributor : Stephan Merz Connect in order to contact the contributor
Submitted on : Wednesday, October 2, 2019 - 5:34:33 PM
Last modification on : Saturday, October 16, 2021 - 11:26:09 AM

File

LIPIcs-ITP-2019-13.pdf
Files produced by the author(s)

Identifiers

`

Citation

Ran Chen, Cyril Cohen, Jean-Jacques Levy, Stephan Merz, Laurent Théry. Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle. ITP 2019 - 10th International Conference on Interactive Theorem Proving, Sep 2019, Portland, United States. pp.13:1 - 13:19, ⟨10.4230/LIPIcs.ITP.2019.13⟩. ⟨hal-02303987⟩

Share

Metrics

Record views

247

Files downloads

793