A Framework for Verifying Depth-First Search Algorithms


Title: A Framework for Verifying Depth-First Search Algorithms
Authors: Peter Lammich and René Neumann (rene /dot/ neumann /at/ in /dot/ tum /dot/ de)
Submission date: 2016-07-05

This entry presents a framework for the modular verification of DFS-based algorithms, which is described in our [CPP-2015] paper. It provides a generic DFS algorithm framework, that can be parameterized with user-defined actions on certain events (e.g. discovery of new node). It comes with an extensible library of invariants, which can be used to derive invariants of a specific parameterization. Using refinement techniques, efficient implementations of the algorithms can easily be derived. Here, the framework comes with templates for a recursive and a tail-recursive implementation, and also with several templates for implementing the data structures required by the DFS algorithm. Finally, this entry contains a set of re-usable DFS-based algorithms, which illustrate the application of the framework.

[CPP-2015] Peter Lammich, René Neumann: A Framework for Verifying Depth-First Search Algorithms. CPP 2015: 137-146

  author  = {Peter Lammich and René Neumann},
  title   = {A Framework for Verifying Depth-First Search Algorithms},
  journal = {Archive of Formal Proofs},
  month   = jul,
  year    = 2016,
  note    = {\url{http://isa-afp.org/entries/DFS_Framework.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Depends on: Automatic_Refinement, CAVA_Automata, Collections, Refine_Monadic
Used by: EdmondsKarp_Maxflow, Refine_Imperative_HOL
Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.