Formalising graph theoretic results with combinatorial optimisation applications

Chair for Logic and Verification

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:

A useful resource on the above material is the following book:

Experience with Isabelle/HOL is required.

Mohammad Abdulaziz, email {mansour} AT []

Prof. Tobias Nipkow, Raum MI 00.09.055, email {nipkow} AT []

Material to read:

Abdulaziz, Mohammad, Kurt Mehlhorn, and Tobias Nipkow. Trustworthy Graph Algorithms. arXiv preprint arXiv:1907.04065 (2019).