Edmonds-Karp 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.68327Lammich, Peter; Sefidgar, S. Reza 2016 all top 5 Cited by 8 Authors 4 Lammich, Peter 2 Sefidgar, S. Reza 1 Doczkal, Christian 1 Hobor, Aquinas 1 Leow, Wei Xiang 1 Mohan, Anshuman 1 Pous, Damien 1 Zhan, Bohua Cited in 1 Serial 4 Journal of Automated Reasoning Cited in 4 Fields 7 Computer science (68-XX) 3 Combinatorics (05-XX) 2 Operations research, mathematical programming (90-XX) 1 Mathematical logic and foundations (03-XX) Citations by Year