COV 883: Special module in TCS

Certifying Algorithms

Announcements The first class is on March 11th (Sunday) at 3:30pm  in Bhart 301
To register at the GIAN portal please click here
Instructor
Prof Kurt Mehlhorn
Overview

A certifying algorithm is an algorithm that produces, with each output, a certificate or witness (easy-to-verify proof) that the particular output has not been compromised by a bug. A user of a certifying algorithm inputs xx, receives the output yy and the certificate ww, and then checks, either manually or by use of a program, that ww proves that yy is a correct output for input xx. In this way, he/she can be sure of the correctness of the output without having to trust the algorithm.

We put forward the thesis that certifying algorithms are much superior to non-certifying algorithms, and that for complex algorithmic tasks, only certifying algorithms are satisfactory. Acceptance of this thesis would lead to a change of how algorithms are taught and how algorithms are researched. The widespread use of certifying algorithms would greatly enhance the reliability of algorithmic software.

The course is based on the LEDA book [MN99] and on a survey on certifying algorithms [MMNS11]. We will also use recent articles on certifying algorithms.
Who can regsiter Senior undergraduate and graduate students who have done a course on Algorithms.
Industry professionals/researchers whose works involves developing/coding advanced algorithms.
Fees
All participants need to complete a one time registration at the GIAN portal (http://www.gian.iitkgp.ac.in/) by paying a fee of Rs 500. After registering at the portal the participant should register for this course [171005K03]. The course fees are
  1. All IITD students: NIL
  2. Undergraduate and Masters students: Rs 1000
  3. PhD students and Postdocs: Rs 5000
  4. Faculty members at Academic Institutions: Rs 10000
  5. Participants from Industry/ Research Organizations: Rs 15000
and should be paid only after the participant has been accepted for the course (you will receive an email to this effect).
Reading Material
[ABMR14] E. Alkassar, S. Boehme, 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. Naeher, and P. Schweitzer. Certifying algorithms. Computer Science Review, 5(2):119-161, 2011.
[MN99] K. Mehlhorn and S. Naeher. 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 Julia M. Badger and Kristin Yvonne Rozier, editors, NASA Formal Methods, volume 8430 of Lecture Notes in Computer Science, pages 46-61. Springer International Publishing, 2014.
Notes and Slides
Tentative Schedule
Date
Time
Topics
Mar 11
1530-1800
Introduction and First examples
Mar 12
1530-1800 More Examples, Testing Planarity of Graphs
Mar 13
1530-1800 Maximum Cardinality Matching in Graphs
Mar 14
1530-1800 Linear Programming Duality and other General Methods for Certification
Mar 15
1530-1800 Certifying Integer Linear Programming, Randomized Certification
Mar 16
1530-1800 Certifying Algorithms and Formal Verification

Evaluation
Evaluation will be through a homework assignment.