Formalizing Network Flow Algorithms: A Refinement Approach in Isabelle/HOL
Formalizing Network Flow Algorithms: A Refinement Approach in Isabelle/HOL
复制标题
DOI：
10.1007/s10817-017-9442-4
复制
发表时间：
2019-02-01
期刊：
影响因子：
--
通讯作者：
Sefidgar, S. Reza
中科院分区：
文献类型：
--
作者：
Lammich, Peter;Sefidgar, S. Reza
我们给出了计算网络中最大流的经典算法的形式化：Edmonds-Karp算法和Push-Relabel算法。我们证明了这些算法的正确性和时间复杂性。我们的形式证明严格遵循标准的教科书证明，即使不是用于形式化的交互定理证明人Isabelle/Holl的专家也可以访问。使用逐步求精技术，我们将通用的Ford-Fulkerson算法实例化为Edmonds-Karp算法，并将Goldberg和Tarjan的通用Push-Relabel算法实例化为Relabel-to-Front算法和FIFO Push-Relabel算法。然后，进一步的改进产生算法的经过验证的高效实现，这与未经验证的参考实现相比是很好的。
We present a formalization of classical algorithms for computing the maximum flow in a network: the Edmonds-Karp algorithm and the push-relabel algorithm. We prove correctness and time complexity of these algorithms. Our formal proof closely follows a standard textbook proof, and is accessible even without being an expert in Isabelle/HOLthe interactive theorem prover used for the formalization. Using stepwise refinement techniques, we instantiate the generic Ford-Fulkerson algorithm to Edmonds-Karp algorithm, and the generic push-relabel algorithm of Goldberg and Tarjan to both the relabel-to-front and the FIFO push-relabel algorithm. Further refinement then yields verified efficient implementations of the algorithms, which compare well to unverified reference implementations.