15-820A: Theorem Proving and Model Checking in PVS

DateTitle / Download
1/15/03Slides: Symbolic Model Checking PS PDF
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/03Slides: Symbolic Model Checking PS PDF
Biere et al.: Symbolic Model Checking without BDDs
1/29/03Slides: SAT PPT PDF
Paper on Chaff (PDF)
Paper on Grasp (PDF)
2/05/03Slides: Computation Tree Logics PS PDF
"Sometimes" and "Not Ever" Revisited: on Branching Versus Linear Time
Expressibility Results for Linear-Time and Branching-Time Logics
2/12/03Slides: 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/03Slides: SMV PPT
Download Cadence SMV
Download NuSMV
2/26/03Slides: Partial Order Reduction PS PDF
State space reduction using partial order techniques
3/5/03Proving Pointer Programs in Higher-Order Logic
3/12/03More on Model Checking with Partial Order Reduction
3/19/03LTL Model Checking with Büchi automata
Slides: LTL Model Checking, Heuristics for Ample Sets, LTL to Büchi automata
3/26/03Spring break, no class
4/2/03SPIN Slides: SPIN, SPIN LTL, SPIN Tool, SPIN Examples
4/9/03Introduction 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/03Proving Theorems Automatically, Semi-Automatically, and Interactively with TPS
Slides: PDF
4/23/03Modeling Hardware and Software with PVS
Slides: PPT
There is also an assignment
4/30/03Proving Software Correct with PVS
Slides: PPT
PVS files used for the class: find.pvs find.prf