COV 883: Special module in TCSCertifying 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 (easytoverify 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
noncertifying 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. 

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


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):241273, 2014. A preliminary
version
appeared under the title Verification of Certifying Computations" in
CAV 2011,
LCNS Vol 6806, pages 6782. [MMNS11] R.M. McConnell, K. Mehlhorn, S. Naeher, and P. Schweitzer. Certifying algorithms. Computer Science Review, 5(2):119161, 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 4661. Springer International Publishing, 2014. 

Notes and Slides 
 
Tentative
Schedule 


Evaluation 
Evaluation will be through a homework assignment. 