Master’s practical course, Master’s thesis, or IDP
Many basic graph theoretic problems are either NP-hard or are not known to be solved in better than impractical polynomial times. This makes solving those problems prohibitive if not impossible for real-world graphs. Approximation algorithms circumvent that by using less resources than exact algorithms, at the expense of providing only approximate solutions. In this project the student would formally verify that 1) the approximate solutions of those algorithms meet a certain quality guarantee and 2) the upper bounds on their runtimes are correct. Particularly interesting algorithms are for computing lower-bounds on (directed) graph diameters and approximate solutions to the All-Pairs-Shortest-Paths problem. Some of those algorithms are deterministic [1,2], and others have elements of randomness in them [3]. A randomised algorithm would be more interesting from a verification perspective.
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]
http://theory.stanford.edu/~rajeev/postscripts/diameter2.ps.gz
[2]
http://danielhlarkin.me/pdfs/soda14-better-approximation-algorithms-for-the-graph-diameter.pdf