### 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

BSD License

### Topics

- Computer science/Algorithms/Graph
- Mathematics/Graph theory

### 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

### Depends on

- The CAVA Automata Library

### Used by

- Transition Systems and Automata
- A Fully Verified Executable LTL Model Checker

### Auto-related entries

- Collections Framework

## Cite

×

Gabow_SCC-AFP

    @article{Gabow_SCC-AFP,
      author  = {Peter Lammich},
      title   = {Verified Efficient Implementation of Gabow's Strongly Connected Components Algorithm},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2014},
      note    = {\url{https://isa-afp.org/entries/Gabow_SCC.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- May 29, 2014 : Isabelle2013-2