Email Gateway (Aug 22 2022 at 13:41): Email Gateway (Aug 22 2022 at 13:41):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
A Framework for Verifying Depth-First Search Algorithms
by Peter Lammich and René Neumann
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
https://www.isa-afp.org/entries/DFS_Framework.shtml
Enjoy!
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Last updated: Apr 24 2024 at 08:20 UTC