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

Lecture slot and venue

Mondays and Thursdays, 02:00-03:20 pm in LH 621 (Lecture Hall Complex) LT2, Block II.

Announcements

• Here are the slides from the lecture on Hoare logic and reasoning about programs.
  
  
• Here is the third assignment for this course. The due date is November 15th. The deadline will not be extended. But feel free to use your unused penalty-free days if you wish to. You do not need to inform me if you are using your penalty-free days.
  
  
• Here are the annotated slides from the online lectures of 30th October and 4th November.
  
  
• We have an extra lecture on Wednesday, 30th October, from 4 pm to 5:20 pm, to compensate for the lecture that we had cancelled on 17th October. This will be an online lecture (on Teams) and we will be recording it.
  
  
• The reference material for the lectures on BMC, k-Induction, and Interpolation based Model Checking has been uploaded on Teams.
  
  
• Here is the webpage from where you can download CBMC binaries. There are plenty of useful resources on the web that can help you get started with CBMC. Here is a short presentation on CBMC by Maria Frade that uses several examples for demonstration. You may also look at the CBMC manual on this page. Here is the set of examples that we had seen in the class.
  
  
• Here is the second assignment for this course. The due date is October 15th. The deadline will not be extended. But feel free to use your unused penalty-free days if you need to. You do not need to inform me if you are using your penalty-free days.
  
  
• For the material covered on ω-regular expressions to NBA, you can look at these slides by B. Srivathsan from CMI. For LTL to NBA, you may look at these and these slides by Srivathsan. You may also look at the Youtube videos of these lectures here.
  
  
• Here is the first assignment for this course. The due date is August 24th. The deadline will not be extended. But feel free to use your penalty-free days if you need to. You do not need to inform me if you are using your penalty-free days.
  
  
• Here is the buggy mutex protocol (implemented in NuSMV) that we had seen in this class. You are expected to fix the implementation and verify using NuSMV that the desired properties hold.
  
  
• NuSMV examples have been uploaded (see the bottom of this page).
  
  
• Please note the change in classroom -- LH 621 (instead of LT2, Block II).
  
  
• Assignment 1 release and due dates have been postponed by a few days. The course calendar has been updated accordingly.
  
  
• We will have an online lecture on 5th August, at this Teams meeting link.
  
  
• We will be using Gradescope for evaluating assignments, quizzes, and exams. Please use the entry code 6JG227 to enrol yourself to this course on Gradescope.
  
  
• Please refer to the logic book by Huth and Ryan (see the Teams channel for this course) for the background material that we have covered so far, on the syntax and semantics of propositional and first-order (predicate) logic.
  
  
• For your reference, here is a link to the last offering of this course.
  
  
• All announcements will be made here (urgent announcements will also be made on Teams). Please do check this section of this page at least once every day.

Course Calendar and Attendance Sheet

Suggested Books and Reference Material

• Logic in Computer Science (Michael Huth and Mark Ryan)
• Model Checking (Edmund Clark, Orna Grumberg, Daniel Kroening, Doron Peled, and Helmut Veith)

Evaluation and Assessment

• Assignments: 24 marks. We will have 3 assignments of 8 marks each. The deadlines for the assignments will not be extended, but every student will be allowed 5 days of penatly-free extension (for all the assignments combined). Any further delay will cost you half marks per hour or part thereof.
  
  
• Quizzes: 24 marks. There will be 5 surprize quizzes in the class of 6 marks each, of which I will count the best 4. If your attendance is more than 75 percent but still you have missed 2 or more quizzes, I will let you write one additional make-up quiz (which won't be a surprize quiz, of course).
  
  
• Minor/Mid-term exam: 20 marks
  
  
• Major/End-term exam: 32 marks
  
  
• Re-exams: There will not be any re-minor exam. If you miss the minor, your marks will be copied (after scaling appropriately) from the major/re-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: For an audit-pass, you must have at least 45 marks in total (excluding the assignment marks). Plus, you must have attended at least 2 surprize quizzes.
  
  
• There will be zero tolerance for dishonest means (including attendance proxy/fraud, copying or sharing solutions in quizzes/exams/assignments, use of mobile phones or other prohibited gadgets, etc.). Offenders will secure an F grade for themselves straight away.

Slides/Reference material

• Propositional and Predicate Logic (Quick recap) -- Please look at the relevant sections (on syntax and semantics of propositional and predicate logic) of the book by Huth and Ryan (see the Teams channel for this course).
  
  
• LTL: Syntax and Semantics -- Here are the slides that give you an outline of what we have covered in the class.
  
  
• NuSMV -- NuSMV tool and documentation may be found here: https://nusmv.fbk.eu/, and here are the NuSMV examples that we worked out in the class.
  
  
• CTL: Syntax, Semantics, and Model Checking -- Please look at Sections 3.4, 3.5 and subsections 3.6.1 and 3.6.2 from the Huth and Ryan book. Here are a few slides that we had used towards the end.
  
  
• BDDs and CTL Model Checking with BDDs -- Please look at Chapter 6, up to Section 6.3.3 from the Huth and Ryan book. Here are the slides that were used in the class.
  
  
• Büchi Automata -- 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. (Some of it has not been covered in the class yet; we will cover it in the next class.)
  
  
• ω-regular expressions, LTL to Büchi Automata -- For the material covered on ω-regular expressions to NBA, you can look at these slides by B. Srivathsan from CMI. For LTL to NBA, you may look at these and these slides by Srivathsan. You may also look at the Youtube videos of these lectures here.
  
  
• CBMC Demo -- Here is the webpage from where you can download CBMC binaries. There are plenty of useful resources on the web that can help you get started with CBMC. Here is a short presentation on CBMC by Maria Frade that uses several examples for demonstration. You may also look at the CBMC manual on this page. Here is the set of examples that we had seen in the class.