Verified Efficient Implementation of Gabow’s Strongly Connected Components Algorithm. 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.
Keywords for this software
References in zbMATH (referenced in 6 articles , 1 standard article )
Showing results 1 to 6 of 6.
- Lammich, Peter: Refinement to imperative HOL (2019)
- Lammich, Peter; Lochbihler, Andreas: Automatic refinement to efficient data structures: a comparison of two approaches (2019)
- Lammich, Peter; Sefidgar, S. Reza: Formalizing network flow algorithms: a refinement approach in Isabelle/HOL (2019)
- Brunner, Julian; Lammich, Peter: Formal verification of an executable LTL model checker with partial order reduction (2018)
- Lammich, Peter; Sefidgar, S. Reza: Formalizing the Edmonds-Karp algorithm (2016)
- Lammich, Peter: Verified efficient implementation of Gabow’s strongly connected component algorithm (2014)