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{https://isa-afp.org/entries/DFS_Framework.html},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Depends on: CAVA_Automata
Used by: Flow_Networks, Refine_Imperative_HOL, Transition_Systems_and_Automata