Abstract
We present an Isabelle/HOL formalization of Gabow's algorithm for
finding the strongly connected components of a directed graph.
Using data refinement techniques, we extract efficient code that
performs comparable to a reference implementation in Java.
Our style of formalization allows for re-using large parts of the proofs
when defining variants of the algorithm. We demonstrate this by
verifying an algorithm for the emptiness check of generalized Büchi
automata, re-using most of the existing proofs.
License
Topics
Session Gabow_SCC
- Gabow_Skeleton
- Gabow_SCC
- Find_Path
- Gabow_GBG
- Gabow_Skeleton_Code
- Gabow_SCC_Code
- Find_Path_Impl
- Gabow_GBG_Code
- All_Of_Gabow_SCC