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.
CITATION STYLE
Lammich, P., & Reza Sefidgar, S. (2016). Formalizing the Edmonds-Karp algorithm. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9807 LNCS, pp. 219–234). Springer Verlag. https://doi.org/10.1007/978-3-319-43144-4_14
Mendeley helps you to discover research relevant for your work.