swMATH ID: 28548
Software Authors: Lammich, Peter; Sefidgar, S. Reza
Description: Formalizing the Edmonds-Karp algorithm. We present a formalization of the Ford-Fulkerson method for computing the maximum flow in a network. Our formal proof closely follows a standard textbook proof, and is accessible even without being an expert in Isabelle/HOL – the interactive theorem prover used for the formalization. We then use stepwise refinement to obtain the Edmonds-Karp algorithm, and formally prove a bound on its complexity. Further refinement yields a verified implementation, whose execution time compares well to an unverified reference implementation in Java.
Homepage: https://www.isa-afp.org/entries/EdmondsKarp_Maxflow.html
Dependencies: Isabelle
Keywords: maximum flow problem; Edmonds-Karp algorithm; push-relabel algorithm; formal verification; Isabelle/HOL; stepwise refinement
Related Software: Gabow SCC; Coq; Isabelle/HOL; Isabelle; Dijkstra Shortest Path; Separation Logic; Archive Formal Proofs; Refinement Monadic; HOL; Graph Theory; Dafny; GitHub; CAVA LTL Modelchecker; Autoref; Why3; MLton; Isar; Boogie; Stony Brook; Stone Algebras
Cited in: 7 Publications

Standard Articles

1 Publication describing the Software, including 1 Publication in zbMATH Year
Formalizing the Edmonds-Karp algorithm. Zbl 1468.68327
Lammich, Peter; Sefidgar, S. Reza

Citations by Year