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.
License
Topics
Session EdmondsKarp_Maxflow
- FordFulkerson_Algo
- EdmondsKarp_Termination_Abstract
- EdmondsKarp_Algo
- Augmenting_Path_BFS
- EdmondsKarp_Impl
- Edka_Checked_Impl
- Edka_Benchmark_Export