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 (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. |
|||||||||||||||||||||
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):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 |
|
|||||||||||||||||||||
Evaluation |
Evaluation will be through a homework assignment. |