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.
This entry is based on our ITP-2016 paper with the same title.