## Estonian Winter School in Computer Science, February - March 2005

Algorithms are problem solving recipes intended for humans; they are usually expressed in a mixture of natural language, mathematical notation, and programming notation. In contrast, programs are intended for machine execution; they are expressed in a programming language.

How do we go from a correct algorithm to a correct program?

The background for my lectures is the experience with LEDA, CGAL, and EXACUS, three algorithm library projects I was involved with.

In the first main part, I discuss certifying algorithms. Certifying algorithms return not only the value they are supposed to compute but also a witness (certificate) which allows the user of the algorithm to convince itself of the correctness of the value returned. I give examples of certifying algorithms and discuss the limits of certification.

In the second main part, I discuss the implementation of geometric algorithms. Their implementation is particularly difficult, because geometric algorithms are usually designed for inputs in general position and for the Real-RAM model of computation. I give examples, how miserably naive implementations can fail, show how to realize a Real-RAM as needed for computational geometry, discuss approaches to overcome the general position problem, and finally come to exact algorithms for curves and surfaces.

• ## LEDA (slides), CGAL,  and  EXACUS

The background for my lectures is the experience with building the systems LEDA, CGAL and EXACUS.
I recommend that you read through the slides of the talk on LEDA.
• The Implementation of Geometric Algorithms

Most algorithms of computational geometry are designed for inputs in general position (no three points on a line, no three lines intersecting, ...) and for the Real-RAM model of computation. However, actual inputs are not necessarily in general position and floating point arithmetic is a coarse approximation of real arithmetic.

• <>The exact computation paradigm: I then discuss the specific problem of computing Arrangement of Conics in the plane. I discuss an exact and complete algorithm which can cope with all inputs. The algorithm implements a Real-RAM as needed for this problem.
• ## Certifying Algorithms

On an input x, a certifying algorithm for a function f does not only return y, the alleged function value f(x), but also a certificate (proof, convincing evidence) of the equality ``y = f(x)''. In this way, a user of the program can convince himself that the program worked correctly on the given input x. We advocate certifying programs as a pragmatic approach to program correctness.
• Certifying Algorithms: this is a survey paper on certifying algorithms. It is still under construction.
• Checking Priority Queues is a short paper which discusses how to check the correctness of priority queues. It appeared in SODA 99.

Prof. Dr. Kurt Mehlhorn
Max-Planck-Institut für Informatik
Algorithms and Complexity Group (AG1)