 May 05: The grades are announced.
 Apr 09: The endterm will be held on April 28th during 10am1pm 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 midterm 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 55.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 midterm 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 safetycritical.
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:
 Formal models of systems: simple programs, boolean encodings (BDDs), state transition diagrams
 Specification logics: propositional, firstorder, temporal
 Algorithmic analysis:
satisfiability checking (SAT), decision procedures for firstorder
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, JoostPieter 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.
 Midterm exams (30%): Two topicwise midterm exams will be conducted.
 Endterm exam (40%): An endterm exam covering the entire course contents will be taken.
Lecture Schedule, Slides, and Study Material
 The slides on propositional and firstorder 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


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
 Firstorder theories (Homework I is be due in the class)
 Lecture 6
  Feb 3, 12
 Equality logic with uninterpreted functions
 Lecture 7+8
  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, FourierMotzkin
 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
  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 (firstorder logic)
   Mar 19
 Class cancelled
   Mar 24, 26
 Computation tree logic (CTL)  Lecture 17+18
  Mar 31
 Ugadi holiday
   Apr 2
 Expressiveness of LTL and CTL  Lecture 19
  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
  Apr 28
 Endterm (all topics covered in the course)
  

