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

Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, Laurent Théry

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.

Published in Proc. ITP 2019, available as: PDF

Reference

@InProceedings{chen:formal,
  author =       {Ran Chen and Cyril Cohen and Jean-Jacques L{\'e}vy
                  and Stephan Merz and Laurent Th{\'e}ry},
  title =        {Formal Proofs of {Tarjan's} Strongly Connected Components
                  Algorithm in Why3, Coq, and Isabelle},
  booktitle =    {10th Intl. Conf. Interactive Theorem Proving},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik},
  year =      2019,
  editor =    {John Harrison and John O'Leary and Andrew Tolmach},
  series =    {LIPIcs},
}

Isabelle formalization

Available here.