!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry EdmondsKarp_Maxflow
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Edmonds-Karp |
AFP entry EdmondsKarp_Maxflow |
Statements
Peter Lammich
0 references
S. Reza Sefidgar
0 references
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.
0 references
0 references
0 references
0 references
12 August 2016
0 references
Formalizing the Edmonds-Karp Algorithm (English)
0 references
