
Kurt Mehlhorn:
Certifying Algorithms:
Algorithmics meets Software Engineering
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 errorprone.
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&\ouml;hme, K. Mehlhorn, and Ch. Rizkallah. A Framework for the
Verification of Certifying Computations. Journal of Automated Reasoning (JAR),
52(3):241273, 2014. A preliminary version appeared under the title "Verification
of Certifying Computations" in CAV 2011, LCNS Vol 6806, pages 6782.
