15-819B Specification, Verification, and Model Checking
("Spec and Check!")
(12 units)
Spring 2004
Edmund M. Clarke and John C. Reynolds
Tuesdays and Thursdays, 1:30-2:50 pm Wean Hall 4615A
Course Description
This course will focus on two of the most successful
approaches to verification: Hoare Logic and Temporal Logic Model
Checking. The goal will be to teach students how to construct proofs
in Hoare Logic and how to use Model Checking tools. Examples will
come mainly from software and protocol verification.
PREREQUISITES: The course is designed to be mostly self-contained. In
particular, a prior logic course is not assumed. Knowledge of
programming languages and concurrency (at the undergraduate level)
will be helpful. Although Model Checking is useful for hardware
verification, no knowledge of computer hardware will be required for
this course.
TEXTS:
(1) Logic in Computer Science: Modeling and Reasoning about Systems by
M. Huth and M. Ryan
(2) Model Checking by E. M. Clarke, Orna Grumberg, and Doron Peled
METHOD OF EVALUATION:
Grading will be based on a set of assignments and a course project.
TOPICS TO BE COVERED:
- Prepositional logic, Predicate calculus, Natural deduction proofs
- Simple Hoare logic, Weakest preconditions
- Hoare logic for arrays and for recursive procedures
- Shared mutable data structures - separation logic
- The Davis-Putnam procedure and modern SAT procedures (Grasp, Chaff, etc.)
- Property specification using Computation Tree Logic (CTL)
- Concurrency (synchronous and asynchronous models), Fairness
- Explicit state model checking
- Binary decision diagrams (BDDs)
- Symbolic model checking
- Detailed introduction to the model checker SMV
- Linear temporal logic (LTL), LTL Tableaux construction, LTL model checking
- Detailed introduction to the model checker SPIN
Course Notes (in Postscript)
Minor corrections have been made to some of these notes since they
were passed out in class. This is indicated by a more recent revision
date.
Homework Assignments (in Postscript)
Last updated: April 1, 2004