• May 05: The grades are announced.
  
• Apr 09: The endterm will be held on April 28th during 10am-1pm in the CSA Lecture Hall.
  
• Apr 09: The third homework is announced. Download it here. It is due in the class on Apr 16.
  
• Apr 09: Practice problems are announced. Download from here.
  
• Apr 09: There would be extra classes on Apr 11 and Apr 14 at 2pm in the CSA Lecture Hall.
  
• Apr 02: Marks of the second mid-term are announced. Contact Pallavi in case of discrepancies.
  
• Mar 19: Today's class is cancelled.
  
• Mar 15: Marks of the second homework are announced. Contact Pallavi in case of discrepancies.
  
• Mar 02: The deadline for the second homework is extended to Mar 7th. It is to be submitted to me in the office on Mar 7th during 5-5.30pm.
  
• Feb 26: The second homework is announced. Download it here. It is due in the class on Mar 5.
  
• Feb 18: Marks of the first mid-term are announced. Contact Shalini in case of discrepancies.
  
• Feb 11: Marks of the first homework are announced. Contact Shalini in case of discrepancies.
  
• Jan 22: The first homework is announced. Download it here. It is due in the class on Jan 29.
  
• Jan 15: The registration details are here. In case of discrepancies, please email Pallavi.
  
• Dec 30: The organizational meeting to be held on Jan 8th in the CSA lecture hall.
  

---

Summary

Computer systems in today's world are large, complex, costly, and often safety-critical. Their correctness is as critical as their performance. While testing is an indispensable technique for exploring behaviors of systems, it can rarely cover all behaviors of the system. Many bugs still make it past testing.

Automated verification is an alternative to testing wherein a formal (mathematical) model of a system is built and analyzed, algorithmically, with respect to logical specifications. Some examples of successful applications of verification to real world systems are IEEE Futurebus+ cache coherence protocol, primary flight control software of Airbus A340, and Windows device drivers. In this course, we will discuss formal modeling of systems and logical specifications of their properties. Our focus will be on understanding the core algorithmic techniques for formal analysis.

The course contents can be summarized as:

1. Formal models of systems: simple programs, boolean encodings (BDDs), state transition diagrams
2. Specification logics: propositional, first-order, temporal
3. Algorithmic analysis: satisfiability checking (SAT), decision procedures for first-order theories (satisfiability modulo theories or SMT for short), temporal logic model checking
   

We will study topics from the following text books during the course. We abbreviate the book titles (underlined) for easy referencing in the suggested reading material below.

• [DP] Daniel Kroening, Ofer Strichman: Decision Procedures: An Algorithmic Point of View, Springer, 2008. Also available online.
• [PMC] Christel Baier, Joost-Pieter Katoen: Principles of Model Checking, MIT Press, 2008.

The following books may be used as additional reading:

• [MC] Edmund M. Clarke, Orna Grumberg, Doron Peled: Model Checking, MIT Press, 2001.
• [LICS] Michael Huth, Mark Ryan: Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press, 2004.
• [CC] Aaron Bradley, Zohar Manna: The Calculus of Computation, Springer, 2007.

Course Evaluation

• Homeworks (30%): Three homework assignments of problem solving nature will be given.
• Mid-term exams (30%): Two topic-wise mid-term exams will be conducted.
• End-term exam (40%): An end-term exam covering the entire course contents will be taken.

---

Lecture Schedule, Slides, and Study Material

• The slides on propositional and first-order logic are adapted from the slides available here.
• The slides on temporal logic are adapted from the slides available here.
• Here are some corrections to the slides.
  

Dates	Topics	Slides	Study Material
Jan 8	Organizational meeting
Jan 13	Propositional logic	Lecture 1	LICS: sec 1.3 and 1.4.1
Jan 15	Propositional logic	Lecture 2	LICS: sec 1.5.1 - 1.5.2 DP: sec 1.3 (ignore the discussion on linear arithmetic and equality logic -- it will be covered later)
Jan 20, 22	SAT solvers (Homework I to be announced)	Lecture 3  Lecture 4a	DP: sec 2.1 - 2.2.3 DP: sec 2.2.4 - 2.2.7
Jan 27	Binary decision diagrams	Lecture 4b + 5a  Lecture 5b	DP: sec 2.3 LICS: sec 6.1 - 6.2
Jan 29	First-order theories (Homework I is be due in the class)	Lecture 6	DP: sec 1.4 - 1.5
Feb 3, 12	Equality logic with uninterpreted functions	Lecture 7+8	DP: sec 3.1 - 3.5
Feb 5	No class
Feb 10	Midterm I (propositional logic)
Feb 17, 19	Equality logic decision procedures	Lecture 9a  Lecture 9b+10  Soundness	DP: sec 4.1 - 4.2 DP: sec 4.3 - 4.4 DP: sec 4.5 - 4.6
Feb 24, 26	Linear arithmetic: simplex (Homework II to be announced)	Lecture 11+12  Notes	DP: sec 5.1 - 5.2.2 DP: sec 5.2.3
Mar 3	Linear arithmetic: branch and bound, Fourier-Motzkin	Lecture 13a  Lecture 13b	DP: sec 5.3 (excluding 5.3.1), 5.4, 5.6
Mar 5	State transition systems (Homework II is due in the class)	Lecture 14	PMC: sec 2.1 - 2.2.4
Mar 10, 12	Linear temporal logic (LTL)	Lecture 15  Lecture 16	PMC: sec 5.1 - 5.1.3 PMC: sec 5.1.4 - 5.1.5 (weak until)
Mar 17	Midterm II (first-order logic)
Mar 19	Class cancelled
Mar 24, 26	Computation tree logic (CTL)	Lecture 17+18	PMC: sec 6.1 - 6.2
Mar 31	Ugadi holiday
Apr 2	Expressiveness of LTL and CTL	Lecture 19	PMC: sec 6.3
Apr 7, 9, 11	LTL model checking (Homework III to be announced)	Lecture 20  Lecture 21  Lecture 22	PMC: sec 5.2 (model checking schema, LTL --> GNBA) PMC: sec 4.3.2 (NBA) PMC: sec 4.3.4 (GNBA --> NBA) PMC: sec 4.4 (product construction and persistence checking by nested DFS)
Apr 14	LTL model checking: soundness and complexity	Lecture 23a  Lecture 23b  Lecture 23c  Lecture 23d	PMC: sec 5.2.1 (complexity) Soundness arguments are scattered across the sections cited above.
Apr 16	CTL model checking	Lecture 24	PMC: sec 6.4
Apr 28	End-term (all topics covered in the course)