Certifying Computations: Algorithmics meets Software Engineering

Talk
Prof. Dr. Kurt Mehlhorn
Max-Planck-Institute for Informatics
Time: 
09.26.2014 11:00 to 12:00
Location: 

CSI Room 2117

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. The top part of the figure above illustrates 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 ([MN99]).

In the first part of the talk, we introduce the concept of certifying algorithms and discuss its significance.. In the second part of the talk, we survey certifying algorithms
([MMNS11]). In the third part of the talk, we discuss the formal verification of certifying
computations ([ABMR14, NRM14]).

[ABMR14] E. Alkassar, S. B¨ohme, K. Mehlhorn, and Ch. Rizkallah. A Framework for the
Verification of Certifying Computations. Journal of Automated Reasoning (JAR),
52(3):241–273, 2014. A preliminary version appeared under the title “Verification
of Certifying Computations” in CAV 2011, LCNS Vol 6806, pages 67 – 82.

[MMNS11] R.M. McConnell, K. Mehlhorn, S. N¨aher, and P. Schweitzer. Certifying algorithms.
Computer Science Review, 5(2):119–161, 2011.

[MN99] K. Mehlhorn and S. N¨aher. The LEDA Platform for Combinatorial and Geometric
Computing. Cambridge University Press, 1999.

[NRM14] Lars Noschinski, Christine Rizkallah, and Kurt Mehlhorn. Verification of certifying
computations through AutoCorres and Simpl. In NASA Formal Methods
Symposium, 2014.