Introduction to Theorem Proving using PVS
Here the materials for the IPA basic course on PVS given at TUE Eindhoven
on 25 June 2008.
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
- Slides [pdf]
- Quick reference [pdf] list of basic tactics plus PVS/Emacs shorthand
- Exercise 1: introduction to propositional, predicate, and
equational logic in PVS:
and prove all lemmas.
- Exercise 2: state machines in PVS (based on example by Harald Ruess):
and prove all lemmas (and complete required definitions) in tripmeter.pvs.
- More exercises to try (by Engelbert Hubbers):