Handouts
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)
15-398 Textbooks

We will be following this textbook for most of the course.

Logic in Computer Science: Modeling and reasoning about systems
Michael R A Huth and Mark D Ryan
Cambridge University Press
The following book is more technical in nature and provides a thorough treatment of model checking.

            Model Checking
            Edmund M. Clarke, Orna Grumberg, Doron Peled
            MIT Press

Other helpful material: The book Computer Aided Verification of Coordinating Processes : The Automata  Theoretic Approach by Robert Kurshan, Princeton series in computer science, is a thorough treatment of automata theoretic verification. The CMU model checking web page at http://www.cs.cmu.edu/~modelcheck has a collection of important links to formal verification resources. Chapter 16 of Volume B of Handbook of Theorecitcal Computer Science by Allen Emerson provides an excellent treatment of modal logics, including temporal logics.