COV 883: Special module in TCS

Certifying Algorithms

Announcements The first class is on March 12th at 3:30pm
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. The course will be available on the portal later this month. The course fees are as under:
  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
Sources
[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.
Tentative Schedule
Date
Time
Topics
Mar 12
1530-1800
Introduction and First examples
Mar 13 1530-1800 More Examples, Testing Planarity of Graphs
Mar 14
1530-1800 Maximum Cardinality Matching in Graphs
Mar 15
1530-1800 Linear Programming Duality and other General Methods for Certification
Mar 16
1530-1800 Certifying Integer Linear Programming, Randomized Certification
Mar 17 (sat)
0900-1130
Certifying Algorithms and Formal Verification

Evaluation
Evaluation will be through a written exam on March 18 (Sun)