Formal Verification of Tarjan's Algorithm
Tarjan’s algorithm computes the strongly connected components of a finite graph using depth-first search.
In this work, we first formalize Tarjan’s Algorithm in an intuitive way, namely the small-step description. We present a proof paradigm (n1-induction) for proving properties on the multi-step relation. Through composition of lemmas, the functional correctness in small-step description can be proved. This part of proof is independent of the implementation, which makes our small step description portable to various implementations.
The small step description turns out to be a bridge that links the model level proof of the graph algorithm and the mechanized verification on a concrete imperative program together. We introduced some techniques, such as share accounting and specification subsumption that make proofs in VST less tedious and more intuitive. Together, the combination of small step description and half-automated proofs in VST ensures the functional correctness of the C program.