|
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 |
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 |
BibTeX: |
@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 = jul,
year = 2016,
note = {\url{http://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 |
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.
|
|