Announcements
- Marks and grades: link
- Course project presentations: April 14 & 16, 2010 (during regular class hours)
- Course project report submission: April 19, 2010 (midnight) by email
(see instructions)
- End-sem exam: April 24, 2010 (10am-1pm)
Introduction
Computer systems in today's world are large, complex, costly, and perhaps 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 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.
Students can tailor the course to their liking by doing a course project in
their area of interest: hardware, software, or embedded systems.
Course contents
- Formal models of systems: state transition diagrams, Kripke structures.
- Specification logics: propositional and first-order logic; temporal logics (CTL, LTL, CTL*); fixpoint logic: mu-calculus.
- Algorithmic analysis: explicit state model checking, symbolic and bounded model checking, decision procedures for satisfiability and satisfiability modulo theories.
- Tools: Student projects involving model checking and satisfiability tools e.g. zChaff, SPIN, NuSMV, PVS.
Reference texts
- Michael Huth, Mark Ryan: Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press, 2004.
- Daniel Kroening, Ofer Strichman: Decision Procedures: An Algorithmic Point of View, Springer, 2008.
- Edmund M. Clarke, Orna Grumberg, Doron Peled: Model Checking, MIT Press, 2001.
- Christel Baier, Joost-Pieter Katoen: Principles of Model Checking, MIT Press, 2008.
Slides and other material
- Propositional logic primer (Lectures 1,2,3):
slides,
slides (modified)
- Satisfiability solvers (Lectures 4,5):
slides,
slides (modified)
- Binary decision diagrams (Lecture 6):
slides,
slides (modified)
- Transition systems (Lecture 7):
slides (Lecture 2),
slides (modified)
- Homework 1:
download (Due on Feb 10, 2010 in the class)
- Linear-time properties - Invariants (Lecture 8):
slides (Lecture 5b)
- Linear-time properties - Safety and Liveness (Lecture 9):
slides (Lecture 6)
- Linear-time properties - Fairness (Lecture 10):
slides (Lecture 7)
- Examination 1: download
- Linear temporal logic (Lecture 11):
slides (Lectures 13, 14)
- Computation tree logic -- CTL, CTL* (Lecture 12):
slides (Lectures 18, 19)
- LTL model checking (Lectures 13, 14, 15):
slides (Lectures 16, 11, 17)
supplementary notes
- Homework 2:
download (Due on March 18, 2010 in the class)
- CTL model checking (Lecture 16):
slides (Lectures 20, 21)
- Symbolic model checking (Lecture 17):
slides
- First order theories (Lecture 18):
slides
- Examination 2: download
- Course project presentation schedule and submission instructions:
link
- Equality logic with uninterpreted functions (Lecture 19):
slides
- Congruence closure and equality graph (Lecture 20):
slides
- Propositional encoding of equality logic (Lecture 21):
slides (1-10)
- Tools used in course projects: SPIN, SATMate, MiniSAT, MiniSAT+, zChaff, Berkmin, WalkSAT, HaifaSAT, TTS, RSAT, SMV, NuSMV, PicoSAT, PB2SAT, GSAT, BMC