We present a formalization of classical algorithms for computing the maximum flow in a network: The Edmonds-Karp algorithm and the push-relabel algorithm. We prove correctness and time complexity of these algorithms. 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.
Using stepwise refinement techniques, we instantiate the generic Ford-Fulkerson algorithm to Edmonds-Karp algorithm, and the generic push-relabel algorithm of Goldberg and Tarjan to both the relabel-to-front and the FIFO push-relabel algorithm. Further refinement then yields verified efficient implementations of the algorithms, which compare well to unverified reference implementations.
Here are the proof documents that are automatically generated by Isabelle. They can be used to get a quick impression of the proof without loading the theories into Isabelle/HOL. The outline documents only contain the definitions and lemmas, the full documents also contain the proofs.