### Abstract

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

### License

BSD License

### Topics

- Computer science/Algorithms/Graph

### Session DFS_Framework

- DFS_Framework_Misc
- DFS_Framework_Refine_Aux
- Impl_Rev_Array_Stack
- On_Stack
- DFS_Chapter_Framework
- Param_DFS
- DFS_Invars_Basic
- DFS_Invars_SCC
- General_DFS_Structure
- Tailrec_Impl
- Rec_Impl
- Simple_Impl
- Restr_Impl
- DFS_Framework
- DFS_Chapter_Examples
- Cyc_Check
- DFS_Find_Path
- Reachable_Nodes
- Feedback_Arcs
- Nested_DFS
- Tarjan_LowLink
- Tarjan
- DFS_All_Examples

### Depends on

- The CAVA Automata Library

### Used by

- Transition Systems and Automata
- Flow Networks and the Min-Cut-Max-Flow Theorem
- The Imperative Refinement Framework
- A Fully Verified Executable LTL Model Checker

## Cite

×

DFS_Framework-AFP

    @article{DFS_Framework-AFP,
      author  = {Peter Lammich and René Neumann},
      title   = {A Framework for Verifying Depth-First Search Algorithms},
      journal = {Archive of Formal Proofs},
      month   = {July},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/DFS_Framework.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jan 14, 2020 : Isabelle2019
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Jul 5, 2016 : Isabelle2016