Interdisciplinary Project (IDP)
Combinatorial optimisation algorithms and proofs of their correctness depend, in many cases, on graph theoretic results. In this project the student would formalise such graph theoretic results in Isabelle/HOL. The formalisation would build on a theory of undirected graphs developed in the context of verifying Edmond’s blossom shrinking algorithm. Examples of interesting topics to formalise there are:
- proving Tutte’s theorem and the Berge-Tutte formula,
- studying ear-decompositions of graphs and their relationship to factor-critical graphs, and
- studying the properties of laminar families.
A useful resource on the above material is the following book:
- Bernhard Korte and Jens Vygen. Combinatorial optimization. Vol. 2. Heidelberg: Springer, 2012.
Prerequisites:
Experience with Isabelle/HOL is required.
Advisor:
Mohammad Abdulaziz, email {mansour} AT [in.tum.de]
Supervisor:
Prof. Tobias Nipkow, Raum MI 00.09.055, email {nipkow} AT [in.tum.de]
Material to read:
[1]
Abdulaziz, Mohammad, Kurt Mehlhorn, and Tobias Nipkow. Trustworthy Graph Algorithms. arXiv preprint arXiv:1907.04065 (2019).