Verified Efficient Implementation of Gabow's Strongly Connected Components Algorithm (Q7361723)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Gabow_SCC
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Verified Efficient Implementation of Gabow's Strongly Connected Components Algorithm |
AFP entry Gabow_SCC |
Statements
28 May 2014
0 references
Peter Lammich
0 references
Verified Efficient Implementation of Gabow's Strongly Connected Components Algorithm (English)
0 references
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.
0 references
0 references
0 references
0 references
0 references
