\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym}
\usepackage{amssymb}
\usepackage[english]{babel}
\usepackage[only,bigsqcap]{stmaryrd}
\usepackage{wasysym}

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}

% Tweaks
\newcounter{TTStweak_tag}
\setcounter{TTStweak_tag}{0}
\newcommand{\setTTS}{\setcounter{TTStweak_tag}{1}}
\newcommand{\resetTTS}{\setcounter{TTStweak_tag}{0}}
\newcommand{\insertTTS}{\ifnum\value{TTStweak_tag}=1 \ \ \ \fi}

\renewcommand{\isakeyword}[1]{\resetTTS\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
\renewcommand{\isachardoublequoteopen}{\insertTTS}
\renewcommand{\isachardoublequoteclose}{\setTTS}
\renewcommand{\isanewline}{\mbox{}\par\mbox{}\resetTTS}



\renewcommand{\isamarkupcmt}[1]{\hangindent5ex{\isastylecmt --- #1}}

%\newcommand{\isaheader}[1]{\section{#1}}

\newcommand{\DefineSnippet}[2]{#2}

\newcommand{\cormen}[1]{[Cormen~$#1$]}


\begin{document}

\title{Formalizing Push-Relabel Algorithms}
\author{Peter Lammich and S.~Reza Sefidgar}
\maketitle

\begin{abstract}
We present a formalization of push-relabel algorithms for computing the 
maximum flow in a network. We start with Goldberg's et al.~generic push-relabel
algorithm, for which we show correctness and the time complexity bound of 
$O(V^2E)$. We then derive the relabel-to-front and FIFO implementation.
Using stepwise refinement techniques, we derive an efficient verified 
implementation.

Our formal proof of the abstract algorithms 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.
\end{abstract}

\clearpage
\tableofcontents

\clearpage

% sane default for proof documents
\parindent 0pt\parskip 0.5ex

\section{Introduction}
Computing the maximum flow of a network is an important problem in graph theory.
Many other problems, like maximum-bipartite-matching, edge-disjoint-paths,
circulation-demand, as well as various scheduling and resource allocating
problems can be reduced to it. 

The practically most efficient algorithms to solve the maximum flow problem
are push-relabel algorithms~\cite{ChGo97}. In this entry, we present 
a formalization of Goldberg's et al.\ generic push-relabel algorithm~\cite{GoTa88}, 
and two instances: The relabel-to-front algorithm~\cite{CLRS09} and the 
FIFO push-relabel algorithm~\cite{GoTa88}. 
Using stepwise refinement techniques~\cite{Wirth71,Back78,BaWr98}, we derive 
efficient verified implementations. Moreover, we show that the generic 
push-relabel algorithm has a time complexity of $O(V^2E)$.

This entry re-uses and extends theory developed for our formalization of
the Edmonds-Karp maximum flow algorithm~\cite{LaSe16,LaSe16_afp}.

While there exists another formalization of the Ford-Fulkerson method in
Mizar~\cite{Lee05}, we are, to the best of our knowledge, the first that verify
a polynomial maximum flow algorithm, prove a polynomial complexity bound, or
provide a verified executable implementation.

% generated text of all theories
\input{session}

\section{Conclusion}\label{sec:concl}
  We have presented a verification of two push-relabel algorithms for solving
  the maximum flow problem. Starting with a generic push-relabel algorithm,
  we have used stepwise refinement techniques to derive the relabel-to-front
  and FIFO push-relabel algorithms. Further refinement yields 
  verified efficient imperative implementations of the algorithms.
  
% optional bibliography
\bibliographystyle{abbrv}
\bibliography{root}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
