CATS-Sep-26-2014

Title

Certifying Computations: Algorithmics meets Software Engineering

Speaker

Kurt Mehlhorn

Abstract

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. Consider the I/O behavior of a conventional program for computing a function f. The user feeds an input x to the program and the program returns an output y. Why should the user believe that y is equal to f(x)?

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 certifying algorithms is accompanied by a checker program C. It 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.

Bio

Kurt Mehlhorn received his PhD in Computer from Cornell University in 1974. He has been a member of the faculty at the Saarland University and a Director at the Max Planck Institute for Computer Science in Saarbruecken. He is the recipient of numerous awards and honors, including the Gottfried Wilhelm Leibniz Prize, the Karl Heinz Beckurts Award, the Konrad Zuse Medal, the EATCS Award, and the ACM Paris Kanellakis Award. He is an ACM Fellow, a Member of the Berlin-Brandenburg Academy of Sciences, a Member of the German Academy of Sciences Leopoldina, and a Foreign Associate of the United States Academy of Engineering. He has received honorary doctorates from the Otto von Guericke University Magdeburg, the Aarhus University, and the University of Waterloo. He served as the Vice President of the Max Planck Society from 2002 to 2008.

Kurt has made fundamental contributions across a vast range of topics in algorithms and data structures, including computational geometry, parallel computing, VLSI design, complexity theory, combinatorial optimization, and graph algorithms. He has authored several books and over 250 scientific publications. Kurt is famous for combining both theoretical work with practical implementation, as demonstrated by his contributions to the famous LEDA Library for Efficient Data Types and Algorithms.

Web Accessibility