Formalizing Network Flow Algorithms: A Refinement Approach in Isabelle/HOL

Abstract

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.