Master's Thesis

The goal of this project is to formalize some graph algorithm, e.g. the blossom algorithm for maximal cardinality matching, in Isabelle/HOL and use refinement techniques to refine the algorithm down to efficiently executable code.

Isabelle/HOL is a theorem prover for higher order logic. In a refinement based top-down development process, an algorithm is first phrased on an abstract level, that is suitable for proving the algorithm correct without coping with implementation details. Then, the algorithm is refined to an efficient implementation, where the refinement is independent of the correctness proof of the algorithm. This allows a separation of concerns between proving the algorithm correct and proving the implementation correct.

The Isabelle Refinement Framework supports such a refinement based top-down development approach, and has already been used for the verification of graph algorithms (Dijkstra's shortest path, Strongly Connected Components).

Tasks:
Choose an interesting graph algorithm (e.g. the blossom algorithm to find a maximum cardinality matching), specify it in Isabelle/HOL using the Refinement Framework, and prove the algorithm correct. If you have enough time, refine the algorithm to an efficient implementation.
Prerequisites:
Experience with Isabelle/HOL (e.g. the Semantics Course by Prof. Nipkow), basic knowledge of graph algorithms (e.g. any undergraduate course covering this topic).
Advisor:
Peter Lammich, Raum MI 00.09.065, email {lammich} AT [in.tum.de]
Supervisor:
Prof. Tobias Nipkow, Raum MI 00.09.055, email {nipkow} AT [in.tum.de]