Certifying Algorithms

Speaker:        Kurt Mehlhorn
                Max-Planck-Institute for Computer Science
                Saarbruecken

Title:          "Certifying Algorithms"

Date:           Monday, June 7 2004

Time:           2:00pm - 3:00pm

Venue:          Lecture Theatre F (Leung Yat Sing Lecture Theatre)
                (near lift nos. 25/26)
                HKUST

                


Abstract:

A program computing a function f from X to Y receives an input x and
returns an output y.  A user must completely trust the program. He/she
sees x and y and has no way to check whether it is indeed the case that
y=f(x).

A certifying algorithm returns in addition a witness w with the property
that knowledge of x, y, and w makes it easy to verify that y=f(x).  By
``easy to verify'' we mean two things. Firstly, there must be a simple
program C (a checking program) that given x, y, and I checks whether
indeed y=f(x).  The program C should be so simple that its correctness is
``obvious''.  Secondly, the running time of C on inputs x, y, and I should
be no larger than the time required to compute f(x) from scratch.  This
guarantees that the checking program C can be used without severe penalty
in running time.

We give a simple example, the task of deciding whether a graph is
bipartite.  A certifying algorithm returns a two-coloring if the input
graph is bipartite and returns an odd cycle if the input graph is not
bipartite.

The design of certifying programs and certifying data structures raises new
algorithmic questions.  We give a survey of results:

- certifying graph algorithms
- checking data structures
- certifying geometric algorithms
- can every algorithm be made certifying?

Many programs in the LEDA library are certifying.

***********************
Biography

Prof. Dr.h.c. Kurt Mehlhorn studied computer science and mathematics at TU
Munich and Cornell University, where he got a PhD in computer science in
1974. He then became a professor at the University of Saarbruecken in
Germany.  Since 1990 he has been director at the Max-Planck-Institute for
Computer Science in Saarbruecken. In 1995 he co-founded Algorithmic
Solutions Software GmbH. Since 2002 he has been Vice President of the
Max-Planck-Society.

His research interests are in data structures, graph algorithms,
computational geometry, algorithm engineering, computational complexity,
and he has been responsible for various successful software libraries like
LEDA, CGAL, EXACUS, and SCIL. He has published about 180 papers and
several books.

He has received numerous awards, like the Leibniz Award of the DFG in
1986, the Karl-Heinz-Beckurts Award in 1994, the Konrad-Zuse Award in
1995, and an honorary doctoral degree from the Otto-von-Guericke
University Magdeburg.  He is an ACM Fellow, member of Academia Europaea,
member of the Berlin-Brandenburgische Akademie der Wissenschaften, and
member of the Deutsche Akademie der Naturforscher Leopoldina. He is has
served as editor for many prestigious journals, like for example
Algorithmica, Information and Computation, SIAM Journal of Computing,
Journal of Discrete and Computational Geometry, etc.