SRI International Computer Science Laboratory
The PVS Verification System
Slides from talks on PVS
Here are slides from some recent talks on PVS and formal methods given
by John Rushby and Shankar. We'll try to make more of our talks
available in this way. You are welcome to use this material (with
attribution) in any talks you wish to give on PVS. Individuals and
organizations are welcome to offer training courses in PVS.
- An overview of PVS using Greatest Comon Divisor (GCD) as an example:
slide show or
postscript
- An introduction to PVS using a Phone Book as an exercise in
requirements analysis:
slide show or
postscript
(corresponding tutorial with links to
specification files)
- Larger examples undertaken in PVS and lessons learned:
slide show or
postscript
- The design rationale for PVS:
slide show or
postscript
- Subtypes in PVS (invited talk at FSE5, 1997):
postscript
(corresponding paper)
- Specification, Proof Checking, and Model Checking for
Protocols and Distributed Systems with PVS (tutorial from FORTE/PSTV '97):
slides and
4-up slides (both
gzipped postscript); also corresponding
text with links to
specification files
- Theorem Proving and Model Checking for Software (Tutorial from FSE4, 1996)
dvi or
postscript
- Theorem Proving and Hardware Verification
dvi or
postscript
- The role of formal methods in the certification of critical systems
dvi or
postscript
(corresponding paper)
Shankar's Marktoberdorf slides on PVS
Back to PVS home page
John Rushby:
Rushby@csl.sri.com