Certifying Computations: Algorithmics meets Software Engineering

Certifying Computations: Algorithmics meets Software Engineering

Kurt Mehlhorn,

Max-Planck-Institute for Informatics


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]).


Kurt Mehlhorn heads the department “Algorithms and Complexity” at the Max Planck Institute for Informatics in Saarbrücken. He is author or co-author of approx. 300 research papers and has published six books. 80 of his former students now hold professorships. Mehlhorn has been awarded a number of prestigious research prizes. These include the Leibniz Prize of the German Research Foundation in 1986 and the Konrad Zuse Medal in 1995. He was Vice President of the Max Planck Society from 2002 to 2008. In 2014, he celebrated his 30th anniversary as a university teacher. He is a member of the Leopoldina, the National Academy of Sciences, of acatech, the National Academy of Science and Engineering, the Academia Europaea, and the Indian National Academy of Engineering. Last year, members of the US National Academy of Science appointed him as a “Foreign Associate” in their ranks. He is the second European computer scientist to be honored this way. In 1995 he co-founded the Algorithmic Solution Software GmbH.


Rodrigo Seromenho Miragaia Rodrigues

Abstract – Annex

The event is finished.


INESC-ID, “Instituto de Engenharia de Sistemas e Computadores: Investigação e Desenvolvimento em Lisboa” is a Research and Development and Innovation Organization (R&D+i) in the fields of Computer Science and Electrical and Computer Engineering. INESC-ID mission is to produce added value to people and society, supporting the response of public policies to scientific, health, environmental, cultural, social, economic and political challenges. INESC-ID promotes cooperation between academia and industry by addressing research on daily life issues, such as healthcare, space, mobility, agri-food, industry 4.0, and smart grids. This high level of knowledge transfer is achieved through both competitive research projects and direct contracted research. Public and private entities have therefore access to a pool of knowledge, resources and services provided through the unique competencies available at the institution.


INESC-ID is supported by:

Contact Us

INESC-ID – Instituto de Engenharia de Sistemas e Computadores, Investigação e Desenvolvimento em Lisboa

INESC-ID headquarters
Rua Alves Redol, 9 – 1000-029 Lisboa – Portugal
+351. 213100300

INESC-ID energy
Av. Rovisco Pais 1 – 1049-001 Lisboa – Portugal
+351. 218417287

INESC-ID taguspark
Avenida Professor Cavaco Silva,
Edifício IST – 2744-016 Porto Salvo – Portugal
+351. 214233508

Join our newsletter

* indicates required

Subscriber consent

The data submitted through this form will be used exclusively for the sending of INESC-ID Newsletter, NEWS-ID, and will not, under any circumstances, be shared with third parties. If you choose to, you can easily unsubscribe from the newsletter by following the link presented in the footer. In that case, your data will be automatically deleted from our information system. If you need to update your contact information or clarify any questions related to the newsletter, please contact info@inesc-id.pt. By submitting this form, you give permission to the use of your personal data according to the conditions above.

We use Mailchimp as our marketing platform. By clicking below to subscribe, you acknowledge that your information will be transferred to Mailchimp for processing. Learn more about Mailchimp's privacy practices here.