Metadata only
Date
2019-02Type
- Journal Article
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. Show more
Publication status
publishedExternal links
Journal / series
Journal of Automated ReasoningVolume
Pages / Article No.
Publisher
SpringerSubject
Maximum flow problem; Edmonds–Karp algorithm; Push–relabel algorithm; Formal verification; Isabelle/HOL; Stepwise refinementOrganisational unit
03634 - Basin, David / Basin, David
More
Show all metadata