| Date | Title / Download |
|---|
| 1/15/03 | Slides: Symbolic Model Checking PS PDF
Handouts:
Clarke et al.: Automatic Verification of Finite-Sate Concurrent System Using Temporal Logic Specifications
Burch et al.: Symbolic Model Checking: 1020 States and Beyond
|
| 1/22/03 | Slides: Symbolic Model Checking PS PDF
Handouts:
Biere et al.: Symbolic Model Checking without BDDs
|
| 1/29/03 | Slides: SAT PPT PDF
Handouts:
Paper on Chaff (PDF)
Paper on Grasp (PDF)
|
| 2/05/03 | Slides: Computation Tree Logics PS PDF
Handouts:
"Sometimes" and "Not Ever" Revisited: on Branching Versus Linear Time
Expressibility Results for Linear-Time and Branching-Time Logics
|
| 2/12/03 | Slides: Counterexample Guided Abstraction Refinement PPT
Clarke, Gupta, Kukula, Strichman: SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques
Chauhan, Clarke, et al.: Automated Abstraction Refinement for Model Checking Large State Spaces using SAT based Conflict Analysis
|
| 2/20/03 | Slides: SMV PPT
Download Cadence SMV
Download NuSMV
|
| 2/26/03 | Slides: Partial Order Reduction PS PDF
Handouts:
State space reduction using partial order techniques
|
| 3/5/03 | Proving Pointer Programs in Higher-Order Logic
|
| 3/12/03 | More on Model Checking with Partial Order Reduction
|
| 3/19/03 | LTL Model Checking with Büchi automata
Slides: LTL Model Checking,
Heuristics for Ample Sets,
LTL to Büchi automata
|
| 3/26/03 | Spring break, no class |
| 4/2/03 | SPIN
Slides: SPIN,
SPIN LTL,
SPIN Tool,
SPIN Examples
|
| 4/9/03 | Introduction to PVS
Slides: PPT
PVS Installation Instructions
PVS Language Reference (how to write theorems)
PVS System Guide (User-Interface, etc.)
PVS Prover Guide (how to make proofs)
|
| 4/16/03 | Proving Theorems Automatically,
Semi-Automatically, and Interactively with TPS
Slides: PDF |
| 4/23/03 | Modeling Hardware and Software with PVS
Slides: PPT
There is also an assignment |
| 4/30/03 | Proving Software Correct with PVS
Slides: PPT
PVS files used for the class:
find.pvs find.prf |
