What is this course about?

This course focuses on the principles and techniques used to automatically verify the correctness of systems. It covers the use of logic to describe system behavior, tools for checking these descriptions, and methods for ensuring reliability. The course combines theory with practical tools like NuSMV and CBMC, showing how abstract concepts can solve real-world problems. Topics include analyzing system properties, converting logical specifications to automata, and verifying software and hardware systems. The goal is to provide a clear understanding of how verification works and its role in building trustworthy systems.

Suggested Books and Reference Material

1. [HR] Logic in Computer Science (Michael Huth and Mark Ryan)


2. [E] A Mathaematical Introduction to Logic (Herbert B. Enderton)


3. [CGKPV] Model Checking (Edmund Clark, Orna Grumberg, Daniel Kroening, Doron Peled, and Helmut Veith)


4. [BHMW] Handbook of Satisfiability (Edited by Armin Biere, Marijn Heule, Hans van Maaren and Toby Walsh)


5. [MB] Satisfiability Modulo Theories: Introduction and Applications (Leonardo De Moura anD Nikolaj Bjorner)

Office Hours

Wednesdays: 10-11.30 am at Bharti 415. If you couldn't follow the previous class or want to discuss the topics covered so far in more detail, I encourage you to make the best use of office hours.

Weekly Feedback

Feedback Form: Here
Your feedback is essential for improving the quality of our lectures. Please share your honest opinions—what went well, what didn’t, and which topics were challenging to understand. This form is anonymous and will take less than 5 minutes to complete. We’d greatly appreciate your thoughts on each class

Lectures (Tentative list)

Evaluation Policy

1. Quizzes: 20% -- 2 quizes each 10%.


2. Assignment: 15%


3. Minor: 25%


4. Major: 35%


5. Class participation: 5% (attendance >= 75% is needed to get 5% marks, else it will be awarded zero.)

• Audit policy: To qualify for an NP grade, you need at least 60% score overall and at least 75% attendance.
• Re-exams:
  There will be no re-minor exams. If you miss the minor exam due to medical reasons, your marks will be appropriately scaled and transferred from the major/re-major exam.
  Only students who obtain prior approval from the instructor before the scheduled date of the minor exam and have a minimum of 75% attendance are eligible for this provision.
  A re-major exam will be conducted only if you miss the regular major exam due to a valid medical reason. Proper medical certification and prior approval are mandatory.
  


• A missed quiz will be awarded zero marks. No requests for a re-quiz will be considered. If you miss the quiz due to medical reason, your marks will be appropriately scaled and transferred from the major exam.
  Only students who obtain prior approval from the instructor before the scheduled date of quiz and have a minimum of 75% attendance overall are eligible for this provision. Proper medical certification are mandatory.


• Late assignment submissions after the deadline are allowed for the next 5 days. However, for each delayed day, a reduction of 5% will be applied. For example, assignment submitted on the deadline will be evaluated for 30%. Assignment submitted one day after the deadline will be evaluated for 25%, and so on. Assignment submitted on the fifth day after the deadline will be evaluated for 5%. Assignment submitted on the sixth day after the deadline will receive no evaluation.


• There will be zero tolerance for dishonest means (including attendance proxy/fraud, copying or sharing solutions/code in quizzes/exams/projects, use of mobile phones or other prohibited gadgets during exam and quizzes, etc.). Offenders will secure an F grade for themselves straight away, and it will be reported to DisCo.