Formal Proofs of Tarjan's 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.

Submitted for publication, available as: PDF

Isabelle formalization

The source files (Isabelle theory and ROOT file for building the theory) are available here. In order to process the theory, you need to download and install Isabelle-2018 and issue the command

isabelle build -D .

from within the directory containing the theory and the ROOT file.

The presentation generated by Isabelle is available here.