Verified Efficient Implementation of Gabow's Strongly Connected Component Algorithm
Verified Efficient Implementation of Gabow's Strongly Connected Component Algorithm
复制标题
经验证的 Gabow 强连通分量算法的高效实现
DOI：
10.1007/978-3-319-08970-6_21
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Peter Lammich
中科院分区：
文献类型：
--
作者：
Peter Lammich
我们提出了一个伊莎贝尔/HOL形式化的Gabow的算法找到强连通组件的有向图。使用数据细化技术，我们提取高效的代码，执行相当于在Java中的参考实现。我们的形式化风格允许重用大部分的证明时，定义算法的变体。我们证明了这一点，通过验证算法的空检查广义Büchi自动机，重用大多数现有的证明。
We present an Isabelle/HOL formalization of Gabow’s algorithm for finding the strongly connected components of a directed graph. Using data refinement techniques, we extract efficient code that performs comparable to a reference implementation in Java. Our style of formalization allows for reusing large parts of the proofs when defining variants of the algorithm. We demonstrate this by verifying an algorithm for the emptiness check of generalized Büchi automata, reusing most of the existing proofs.