@inproceedings{f7a740143a8346deb2121678ad8e145e,

title = "Formalizing the Edmonds-Karp Algorithm",

abstract = "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.",

author = "Peter Lammich and Sefidgar, {S. Reza}",

year = "2016",

month = aug,

day = "7",

doi = "10.1007/978-3-319-43144-4_14",

language = "English",

series = "Interactive Theorem Proving",

pages = "219--234",

booktitle = "International Conference on Interactive Theorem Proving",

}