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 reusing 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, reusing most of the existing proofs. © 2014 Springer International Publishing.
Cite
CITATION STYLE
Lammich, P. (2014). Verified efficient implementation of Gabow’s strongly connected component algorithm. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8558 LNCS, pp. 325–340). Springer Verlag. https://doi.org/10.1007/978-3-319-08970-6_21
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
