Note: This is an archvied version of our old webpage. Some links might be broken. The current one can be found here.
I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
Publications - A Framework for Verifying Depth-First Search Algorithms

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

This work is not available online here.