Formalizing the Edmonds-Karp Algorithm

Peter Lammich, S. Reza Sefidgar

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

450 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationInternational Conference on Interactive Theorem Proving
Pages219-234
Number of pages15
DOIs
Publication statusPublished - 7 Aug 2016

Publication series

NameInteractive Theorem Proving
Volume9807
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Dive into the research topics of 'Formalizing the Edmonds-Karp Algorithm'. Together they form a unique fingerprint.

Cite this