[Club2] Rehearsal-Talk for ITP 2016: Formalizing the Edmonds-Karp Algorithm

[Peter Lammich]

Friday, Aug 5, 14:00 in Turing

Speaker: Peter Lammich

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 be-
ing 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.