Formal Proof of the Push-relabel Algorithm in Coq
Name
Aksel Õim
Abstract
The push-relabel algorithm calculates the maximum flow in a flow network by giving nodes height and excess values. The algorithm tries to send the excess from the nodes to the sink by continually changing the height of the nodes and preserving three different invariants. The main goal of this bachelor's thesis is to formally prove the push-relabel algorithm in Coq by giving an overview of the implementation of the algorithm and proven lemmas. The main focus is on the proof to the algorithm, but an overview of Coq and graph definitions will be given along with a description of the push-relabel algorithm.
Graduation Thesis language
Estonian
Graduation Thesis type
Bachelor - Computer Science
Supervisor(s)
Kalmer Apinis
Defence year
2024