- 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:
- Formal models of systems: simple programs, boolean encodings (BDDs), state transition diagrams
- Specification logics: propositional, first-order, temporal
- 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
|
|
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
| | 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, 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
| | 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
| | 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
| End-term (all topics covered in the course)
| | |
|
|