Master’s Thesis, Bachelor’s Thesis
The goal of this project is to formalize some algorithm (e.g. the Hopcroft-Karp algorithm for maximal cardinality matching in bipartite graphs, Johnson’s algorithm, topological sort …) or efficient data structure 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 efficient algorithms (Dijkstra’s shortest path, Strongly Connected Components, Network Flow, …) and data structures (Hash Maps, Union Find, …).
Additionally, similar techniques can be used to formally prove the run-time behaviour of the verified algorithms and data structures.
Tasks:
Choose an interesting 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. Next, refine the algorithm to an efficient implementation. If you have enough time, formalize the run-time analysis of the algorithm.
OR:
Choose an interesting algorithm that has already been verified and additionally verify the run-time bounds of that algorithm or data structure.
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).
Supervisor:
Prof. Tobias Nipkow, Raum MI 00.09.055, email {nipkow} AT [in.tum.de]