### 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. It is accessible even without being an expert in Isabelle/HOL, the interactive theorem prover used for the formalization.

### License

BSD License

### Topics

- Computer science/Algorithms/Graph
- Mathematics/Graph theory

### Session Prpu_Maxflow

- Generic_Push_Relabel
- Prpu_Common_Inst
- Fifo_Push_Relabel
- Graph_Topological_Ordering
- Relabel_To_Front
- Prpu_Common_Impl
- Fifo_Push_Relabel_Impl
- Relabel_To_Front_Impl
- Generated_Code_Test

### Depends on

- Flow Networks and the Min-Cut-Max-Flow Theorem

### Auto-related entries

- Formalizing the Edmonds-Karp Algorithm
- Isabelle/Solidity: A deep Embedding of Solidity in Isabelle/HOL
- A Verified Imperative Implementation of B-Trees
- Pop-Refinement
- Psi-calculi in Isabelle

## Cite

×

Prpu_Maxflow-AFP

    @article{Prpu_Maxflow-AFP,
      author  = {Peter Lammich and S. Reza Sefidgar},
      title   = {Formalizing Push-Relabel Algorithms},
      journal = {Archive of Formal Proofs},
      month   = {June},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/Prpu_Maxflow.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jan 14, 2020 : Isabelle2019
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Jun 2, 2017 : Isabelle2016-1