Instructor: Kumar Madhukar (madhukar)
Office address: 516, 4th floor, Bharti building

Announcements

• The reference material for all the lectures has been indicated/uploaded in the Lectures section at the bottom of this page.
  
  
• The content on DFA Learning and Assume-Guarantee reasoning has been excluded from the syllabus of the final quiz/exam.
  
  
• Instead of the usual class on Monday, 20th March, we will have an online class (on Monday itself). The online class, however, will start at 01:00 pm and end at 02:20 pm. The lecture will be recorded so that you can view it later at your convenience.
  
  
• We will have an online lecture on March 6th (at the class time, 1400-1520), to make-up for the lecture cancelled on Feb 13. This lecture will be recorded so that you can view it later at your convenience.
  
  
• We will have the first quiz either on 28th Jan, or on 30th Jan. If you are absent on the day of the first quiz, I will allow you to write a re-quiz on Friday, 3rd Feb, from 3:00-4:30 pm in my office. Please also note that the remaining quizzes will be surprize quizzes and you won't get an opportunity for a re-quiz in those.
  
  
• Please note the change in the classroom for our lectures. The classes will happen in IIA 305 (2nd floor, Bharti building).
  
  
• If you have any doubts/questions/clarifications to discuss with me, please do so during the office hours (see above). If you would like to meet me outside the office hours, in-person or online, please send an email to set-up an appointment. You may, of course, catch me at the end of every lecture without a prior appointment.
  
  
• All announcements will be made here. Please do check this section of this page at least once every day.

Suggested Books and Reference Material

• Model Checking (Edmund Clark, Orna Grumberg, Daniel Kroening, Doron Peled, and Helmut Veith)
• Logic in Computer Science (Michael Huth and Mark Ryan)
• Finite-state Automata on Infinite Inputs (Madhavan Mukund)
• Srivathsan's slides on LTL Model Checking (LTL to Büchi automata). These slides are based on Srivathsan's NPTEL course on Model Checking.
• Learning Regular Sets from Queries and Counterexamples (Dana Angluin's original 1987 paper)
• Learning Assumptions for Compositional Verification (paper from TACAS 2003)

Lecture slot

Mondays and Thursdays, 02:00-03:20 pm in IIA 305 (2nd floor, Bharti building)

Evaluation and Assessment

• Assignments: 24 marks. We will have 4 assignments of 6 marks each. The deadlines for the assignments will not be extended, but every student will be allowed 8 days of free extension (for all the assignments combined, which you may use anyhow). Additional delays will cost you 3 marks per day.
  
  
• Quizzes: 20 marks. There will be 4 surprize quizzes in the class (at any time during the class), of 7 marks each. There cannot be any make-up surprize quizzes, of course, but I will count the total marks for quizzes as min(20,s) where s is the sum of all your quiz marks.
  
  
• Minor I: 14 marks
  
  
• Minor II: 14 marks
  
  
• Major: 28 marks
  
  
• Re-exams: There will not be any re-minor exam for those crediting the course. If you miss a minor exam, your marks will be copied (after scaling appropriately) from the next exam in which you appear, in this order: Minor I ← Minor II ← Major. A re-major exam will be held if required, of course.
  
  
• Grading: We will adopt a relative grading scheme.
  
  
• Pass: 30 marks or more.
  
  
• Audit: At least 50% 40% percent marks in every minor and major exam, and at least 14 11 marks in all the quizzes combined. Note, however, that if you are auditing, your marks won't be scaled and copied from the next exam if you miss one of the minors or the major exam. We will have re-exams for you.
  
  
• There will be zero tolerance for dishonest means like copying solutions from others, and even letting others copy your solution, in any quiz/exam/assignment. If you are found indulging in such an activity, your answer paper will not be evaluated and your participation/submission will not be counted. Second-time offenders will be summarily awarded an F grade.

Lectures

• Week 1 (5th and 9th Jan 2023)
  Topics: Brief recap of propositional and predicate logic; Introduction to LTL (syntax and semantics)
  Additional Remarks: For LTL syntax and semantics, please refer to Chapter 3 of the book Logic in Computer Science book by Huth and Ryan, up to Sec. 3.2.2. The background on propositional and predicate logic (syntax and semantics, notions of satisfiability, validity and semantic entailment, normal forms) can be covered from the first two chapters of the same book.
  
  
• Week 2 (12th and 16th Jan 2023)
  Topics: Specifications in LTL, formula equivalence, adequate set of connectives, and NuSMV
  Additional Remarks: Here are the slides that were used in the class. For reference material, please refer to Chapter 3 of the book by Huth and Ryan (Sec. 3.2.3--3.3.6). The NuSMV tool and documentation may be found here: https://nusmv.fbk.eu/, and here are the NuSMV examples that we had looked at.
  
  
• Week 3 (19th and 23rd Jan 2023)
  Topics: CTL Model Checking
  Additional Remarks: Here are the slides that were used in the class. For reference material, please refer to Chapter 3 of the book by Huth and Ryan (Sec. 3.4--3.6.1).
  
  
• Week 4 (28th and 30th Jan 2023)
  Topics: CTL Model Checking and Binary Decision Diagrams
  Additional Remarks: Here are the slides that were used in the class for CTL Model Checking. For BDDs, we used these slides. For reference material, on BDDs, please refer to Chapter 6 of the book by Huth and Ryan (up to Sec. 6.2).
  
  
• Week 5 (2nd and 13th Feb 2023)
  Topics: CTL Model Checking (with fairness) using BDDs
  Additional Remarks: Here are the slides that were used in the class. For reference material, please refer to the book by Huth and Ryan (Sections 3.6.1, and 6.3).
  
  
• Week 6 (16th and 20th Feb 2023)
  Topics: Recap of CTL model checking with fairness, and Büchi automata
  Additional Remarks: For the content covered on Büchi automata, please look at the first 9 pages of the notes on Finite-state Automata on Infinite Inputs by Madhavan Mukund.
  
  
• Week 7 (23rd and 27th Feb 2023)
  Topics: LTL Model Checking
  Additional Remarks: Here are the slides that contain (or provide a link to) the material covered in the class. Here are the slides on LTL Model Checking (LTL to Büchi automata) that we had used in the class on 27th Feb. These slides are by B. Srivathsan from CMI. They are based on Srivathsan's NPTEL course on Model Checking.
  
  
• Week 8 (2nd and 13th Mar 2023)
  Topics: Extra lecture (make-up for Feb 13th); Propositional SAT Solving
  Additional Remarks: Here are the slides for the extra lecture on March 6th. The slides of the first (of the two) lectures on SAT solving are available here. The slides of the second lecture on SAT can be found here.
  
  
• Week 9 (16th and 20th Mar 2023)
  Topics: Bounded Model Checking, k-Induction
  Additional Remarks: This lecture's recording is available on Teams. Here is a link to the scribbled notes from the lecture.
  
  
• Week 10 (27th and 29th Mar 2023)
  Topics: Interpolation and SAT-Based Model Checking
  Additional Remarks: Here are the slides that cover the material discussed in the class. Please also look at the notes on interpolation (itp-notes.pdf) uploaded on Teams.
  
  
• Week 11 (3rd and 6th Apr 2023)
  Topics: SAT-Based Model Checking without Unrolling (IC3)
  Additional Remarks: Here are the slides that cover the material discussed in the class. Here is Aaron Bradley's homepage where you may find useful relevant material on this topic.
  
  
• Week 12 (10th and 13th Apr 2023)
  Topics: Hoare logic, CBMC demo
  Additional Remarks: Here are the slides on Hoare logic. CBMC demo was done online (recording available on Teams). The examples used in the demo are available here (and also on Teams).
  
  
• Week 13 (17th and 20th Apr 2023)
  Topics: Predicate Abstraction and CEGAR
  Additional Remarks: Here are the slides on predicate abstraction and counterexample-guided abstraction-refinement. Many of these slides have been borrowed from a tutorial presentation on this topic by Daniel Kroening at SRI (which is an excellent resource on this topic; and can be found here).
  
  
• Week 14 (24th and 27th Apr 2023)
  Topics: DFA Learning, Assume-Guarantee Reasoning
  Additional Remarks: The material that I covered in the class was mostly from these two papers: Learning Regular Sets from Queries and Counterexamples (Dana Angluin's original 1987 paper), and Learning Assumptions for Compositional Verification (paper from TACAS 2003). Here is an excellent set of slides on L* algorithm by Deepak D'Souza from IISc.