COV 883: Special module in TCS
|Announcements||The first class is on March 12th at 3:30pm
||Prof Kurt Mehlhorn|
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
Industry professionals/researchers whose works involves developing/coding advanced algorithms.
||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:
||[ABMR14] E. Alkassar, S.
Boehme, K. Mehlhorn, and Ch.
Rizkallah. A Framework for the Verification of Certifying Computations.
of Automated Reasoning (JAR), 52(3):241-273, 2014. A preliminary
appeared under the title Verification of Certifying Computations" in
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.
||Evaluation will be through a
written exam on March 18 (Sun)