Formalization of Tarjan's Algorithm in Isabelle

This work is part of a comparative study on verifying Tarjan's algorithm for computing strongly connected components in a graph in three different proof assistants: Why3, Coq, and Isabelle. All three formalizations are available here.

The accompanying publication appeared in ITP 2019 and is described here.

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 and issue the command

isabelle build -D .

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

You can also browse the presentation generated by Isabelle.

Stephan Merz