E0223: Automated Verification
January - April 2014
Instructor: Aditya Kanade
Office hours: Thur, 4-5pm
        (by prior email appointment only)

Class Venue: CSA Lecture Hall (117)
Class Timings: Mon/Wed, 2-3.30pm

TAs: Anirudh Santhiar, Pallavi Maiya, Shalini Kaleeswaran, Soham Ghosh


Announcements
  • 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)