A Framework for Verifying Depth-First Search Algorithms
A Framework for Verifying Depth-First Search Algorithms
复制标题
验证深度优先搜索算法的框架
DOI：
10.1145/2676724.2693165
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
René Neumann
中科院分区：
文献类型：
--
作者：
Peter Lammich;René Neumann
许多图算法都是基于深度优先搜索（DFS）的。这些算法的形式化通常具有许多共同的思想。在本文中，我们将这些想法总结成Isabelle/HOL中的一个框架。基于Isabelle精化框架，我们为基于DFS的算法的基于精化的开发提供支持，从措辞和证明抽象算法的正确性，到选择适当的实现风格（例如，作为一个案例研究，我们验证了不同复杂度的DFS算法，从一个简单的循环检查器，在一个安全属性模型检查器，复杂的算法，如嵌套DFS和Tarjan的SCC算法。
Many graph algorithms are based on depth-first search (DFS). The formalizations of such algorithms typically share many common ideas. In this paper, we summarize these ideas into a framework in Isabelle/HOL.Building on the Isabelle Refinement Framework, we provide support for a refinement based development of DFS based algorithms, from phrasing and proving correct the abstract algorithm, over choosing an adequate implementation style (e.g., recursive, tail-recursive), to creating an executable algorithm that uses efficient data structures.As a case study, we verify DFS based algorithms of different complexity, from a simple cyclicity checker, over a safety property model checker, to complex algorithms like nested DFS and Tarjan's SCC algorithm.