COL 750 Foundations of Automatic Verification

General Information

Semester: II, 2021-2022
Timings: Mon/Thur 15:30-17:00 (Slot AB)
TA: Tooba Khan (email: Tooba.Khan.jcs21@csia.iitd.ac.in)

Course Outline

The main focus of this course is learn foundational concepts for assessing reliability of systems, viz., model checking. Establishing reliability of systems assume importance when they are deployed in complex and mission critical settings such as in automotives, aircrafts, pacemakers, etc. This course will introduce techniques for modeling(transformational and reactive) systems along with a comprehensive description of various tools and algorithms to verify system models against a set of correctness properties (such as safety, liveness, etc.). For a broad list of topics that will be covered in this course, please refer COL750 course plan.

Honour Code

• All students are expected to follow the highest ethical standards.
• Collaborations and discussions are encouraged. However, all students are required to write up all solutions entirely on their own. Any collaboration, or help taken, must be declared.
• Students are encouraged to refer to books, papers and internet resources. They may even consult other individuals. However, the source must be clearly cited if any part of the solution (or even an idea) is taken from such a source.
• Failure to declare any help taken will be interpreted as academic misconduct.
• Copying (in whole or in part) from others is deemed cheating and those who enable this activity either deliberately or through negligence are also deemed to have cheated. Cheating is a serious academic misconduct; it will attract a summary F grade to the involved students and referral to the discplinary committee.

Important Note to the Students

• All academic matters, doubts etc. should be cleared during the lectures/tutorials or immediately after them, in the presence of the whole class, so that the clarifications does not have to be communicated to others separately.

• In an online semester, when quizzes are announced beforehand, make adequate back-up arrangements for power failures and lack of internet connections, and have enough time for downloading and uploading your answers. No excuses for these will be considered valid.

• Absence in quizzes will result in 0 for that quiz. Make-up quizzes will not be given out. A more elaborate note to the students can be found here

• Attendance: The Institute requires a mandatory 75% attendance for all students, which includes time lost due to illness. However this course will require 100% attendance. Please inform the instructor if for any reason you cannot attend a class. Be warned that it will be difficult to make up if you miss classes.

• Illness: In sickness or ill-health, a Medical Certificate from the Institute Sick Bay, or a doctor from an Institute-recognised hospital is necessary, especially if you request for a make-up test. Only in the case of serious illnesses will I consider giving an extension on assignments.

• Make-up Tests: Make-up tests (minor or major exams only) will be given only when the student furnishes a valid documentation of illness for a period including the day of the exam.

Grading Policy

• Quizzes: 15%
• Assignments: 35%
• Minor Exam: 20%
• Major Exam: 30%

As per the Institute regulations, an A grade will be awarded only over 80% and no student with less than 30% will be given a passing grade.

An I grade will be awarded only in the case of an illness during the major exam. A make-up exam will be scheduled at the earliest, and the I grade will be converted as soon as possible. However, please do your best to ensure that you donot break a leg or otherwise fall ill during examinations. Repeat examinations are harder by tradition.

References

The course material will primarily drawn from the following two sources

• Christel Baier and Joost-Pieter Katoen: Principles of Model Checking (PMC)
• Edmund M. Clarke, Orna Grumberg, and Doron A. Peled: Model Checking (MC)

For particular topics not covered in the books, I will provide separate references which may include research papers.

Class notes and Programs developed in the class

Lecture notes will be available on Moodle.