Date | Day | Title |
08/27/02 | Tuesday | Model checking overview (pdf) |
08/29/02 | Thursday | Propositional logic (ps) (pdf) |
09/03/02 | Tuesday |
Lecture on GRASP
(ps)
(pdf)
(ppt) GRASP technical report (ps) (pdf) |
09/17/02 | Tuesday | Binary Decision Diagrams (ps) (pdf) |
09/19/02 | Thursday | Binary Decision Diagrams (cont.) (ps) (pdf) |
09/24/02 | Tuesday | Binary Decision Diagrams (cont.) |
09/26/02 | Thursday |
CTL Model Checking
(ps)
(pdf) Examples (tgz) (zip) |
10/01/02 | Tuesday | SMV Examples (tgz) (zip) |
10/03/02 | Thursday | SMV, NuSMV, and CadenceSMV (ppt) |
10/08/02 | Tuesday |
Example: a bus protocol
(ppt) Code (tgz) (zip) |
10/10/02 | Thursday |
Semantics of CTL
(ps)
(pdf) |
10/15/02 | Tuesday |
Explicit State Model Checking
(ps)
(pdf) |
10/17/02 | Thursday |
Symbolic Model Checking
(ps)
(pdf) |
10/24/02 | Thursday |
Basic Fixpoint Theorems
(ps)
(pdf) |
10/24/02 | Thursday |
How model checkers work
(ps)
(pdf) |
11/14/02 | Thursday |
CTL, LTL, CTL* - An example - Updated!
(ppt)
(pdf) SPIN - Checking LTL properties (ppt) (pdf) SPIN - Running the tool (ppt) (pdf) |
11/19/02 | Tuesday |
SPIN - Examples
(ppt)
(pdf) |
11/21/02 | Thursday |
Bounded Model Checking
(ps)
(pdf) |
12/3/02 | Tuesday |
Counterexample guided abstraction refinement
(ps)
(pdf) |
We will be following this textbook for most of the course.
Logic in Computer Science: Modeling and reasoning about systemsThe following book is more technical in nature and provides a thorough treatment of model checking.
Michael R A Huth and Mark D Ryan
Cambridge University Press
Model
Checking
Edmund M. Clarke, Orna Grumberg, Doron Peled
MIT Press