Reference:

Rene Neumann. A framework for verified depth-first algorithms. In Annabelle McIver and Peter Höfner, editors, Proc. of the Workshop on Automated Theory Exploration (ATX 2012), pages 36–45. EasyChair, 2012.

Abstract:

We present a framework in Isabelle/HOL for formalizing variants of depth-first search. This framework allows to easily prove non-trivial properties of these variants. Moreover, verified code in several programming languages including Haskell, Scala and Standard ML can be generated.

In this paper, we present an abstract formalization of depth-first search and demonstrate how it is refined to an efficiently executable version. Further we use the emptiness-problem of Büchi-automata known from model checking as the motivation to present three Nested DFS algorithms. They are formalized, verified and transformed into executable code using our framework.

Suggested BibTeX entry:

@inproceedings{RNATX12,
    author = {Rene Neumann},
    booktitle = {Proc. of the Workshop on Automated Theory Exploration (ATX 2012)},
    editor = {Annabelle McIver and Peter H\"ofner},
    pages = {36--45},
    publisher = {EasyChair},
    title = {A Framework for Verified Depth-First Algorithms},
    year = {2012}
}