Formal Verification of Edmond’s Blossom Algorithm
Interactive theorem provers have been used in a number of impressive formal proofs ranging from the Kepler conjecture to C compilers and operating systems, but much less so in the realm of efficient algorithms. We report on the formal proof of the correctness of a functional formulation of Edmond’s blossom algorithm for maximum matchings. Generally, there are two challenges in verifying an algorithm at an abstract level, i.e. not to verify the implementation. The first is to formulate it in a language that has support for verification. The second is to formally prove the lemmas needed for the algorithm’s correctness argument, which may not all be explicitly stated, let alone proven, in the literature. What sets the blossom algorithm apart from other fundamental algorithms, like Dijkstra’s or Ford-Fulkerson, is that the second of the two aforementioned challenges is much more emphasised in its verification. In particular, the verification of the blossom algorithm needs a subtantial library of formalised graph theory to prove Berge’s lemma and the graph theoretic argument behind the correctness of blossom contraction, which is the main step in the algorithm. This project is in collaboration with Kurt Mehlhorn and Tobias Nipkow.
Mohammad Abdulaziz is a postdoctoral researcher in the Technical University of Munich at the Chair for Logic and Verification. He obtained his PhD in 2018 from The Australian National University. His research concerns the application of theorem proving to the verification of algorithms. This includes the verification of graph algorithms, algorithms for AI planning and the development of libraries of formal mathematics that facilitate algorithm verification.