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)

1 Institute of Software Chinese Academy of Sciences [Beijing]
2 MSR - INRIA - Microsoft Research - Inria Joint Centre
3 PI.R2 - Design, study and implementation of languages for proofs and programs
4 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
5 MOSEL - Proof-oriented development of computer-based systems
6 MARELLE - Mathematical, Reasoning and Software
7 STAMP - Sûreté du logiciel et Preuves Mathématiques Formalisées

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.

Mots clés: Mathematical logic; Program verification; Graph algorithm; Formal proof

Domaines: Logique en informatique [cs.LO]

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⟩