Speaker: Kurt Mehlhorn, Max Planck Institute for Informatics and Saarland University
Title: Certifying Computations
I am mostly interested in algorithms for difficult combinatorial and geometric problems: what is the fastest tour from A to B? How to optimally assign jobs to machines? How can a robot move from one location to another one? Algorithms solving such problems are complex and their implementation is error-prone.
How can we make sure that our implementations of such algorithms are reliable? Certifying algorithms are a viable approach towards the goal. A conventional program for computing a function f works as follows. The user feeds an input x to the program and the program returns an output y. A certifying algorithm for f computes y and a witness (proof) w; w proves that the algorithm has not erred for this particular input. The checker C accepts the triple (x,y,w) if and only if w is a valid witness for the equality y =f(x). Certifying algorithms are the design principle for LEDA, the library of efficient data types and algorithms.
In the first part of the talk, we introduce the concept of certifying algorithms. In the second part of the talk, we discuss a certifying algorithm for three-connectivity of graphs. In the third part of the talk, we discuss a framework for the formal verification of certifying computations.