Introduction to Theorem Proving using PVS
Here the materials for the IPA basic course on PVS given at TUE Eindhoven
on 25 June 2008.
- Slides [pdf]
- Quick reference [pdf] list of basic tactics plus PVS/Emacs shorthand
- Exercise 1: introduction to propositional, predicate, and
equational logic in PVS:
download
pvs_intro.pvs
and prove all lemmas.
- Exercise 2: state machines in PVS (based on example by Harald Ruess):
download
machine.pvs
and
tripmeter.pvs
and prove all lemmas (and complete required definitions) in tripmeter.pvs.
- More exercises to try (by Engelbert Hubbers):
PVS can be downloaded from the PVS webpages at SRI. There is also more documentation there, namely
If you're trying to use PVS by yourself, the WIFT tutorial, reachable
from PVS documentation webpage is a good place to start; pages 32-.. talk you through getting started
with PVS.