Reference:

Peter Lammich and Rene Neumann. A framework for verifying depth-first search algorithms. In CPP, January 2015.

Abstract:

Many graph algorithms are based on depth-first search (DFS). The formalizations of such algorithms typically share many common ideas. In this paper, we summarize these ideas into a framework in Isabelle/HOL. Building on the Isabelle Refinement Framework, we provide support for a refinement based development of DFS based algorithms, from phrasing and proving correct the abstract algorithm, over choosing an adequate implementation style (e. g., recursive, tail-recursive), to creating an executable algorithm that uses efficient data structures. As a case study, we verify DFS based algorithms of different complexity, from a simple cyclicity checker, over a safety property model checker, to complex algorithms like nested DFS and Tarjan’s SCC algorithm.

Suggested BibTeX entry:

@inproceedings{CPP,
    author = {Peter Lammich and Rene Neumann},
    booktitle = {CPP},
    month = {January},
    title = {A Framework for Verifying Depth-First Search Algorithms},
    year = {2015}
}