IPA introductory course on PVS

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):
- Liar paradox liar.pvs
- Knaster-Tarski theorem KnasterTarski.pvs

PVS can be downloaded from the PVS webpages at SRI. There is also more documentation there, namely

System Guide, which gives info about using PVS system
Language Manual, which gives info about the syntax of PVS specification language
Prover Guide, which explains all the prover tactics

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.