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

Ran Chen, Cyril Cohen, Jean-Jacques Lvy, Stephan Merz, Laurent Thry

Browse the full ITP paper archive.