This tutorial introduces some of the more powerful strategies provided by the PVS theorem prover. It consists of two parts: the first extends a previous tutorial by Ricky Butler (dvi or postscript) demonstrating how his proofs may be performed in a more automated manner; the second uses the ``unwinding theorem'' from the noninterference formulation of security to introduce theorem-proving strategies for induction that cannot be demonstrated in the framework of Ricky Butler's example.
Using the more powerful strategies of PVS to automate easy proofs (and the easy parts of hard proofs) frees users to concentrate on truly difficult proofs. Automation also makes proofs more robust to changes in the specification, thereby facilitating active design exploration and adaptation to changed requirements.
This tutorial also shows how specifications and proofs may be better presented using the LaTeX and PostScript generating facilities of PVS.
Paper:
postscript
PVS specification files
Ricky Butler's original version
Treatment in
Mizar by Piotr Rudnicki (cf. Appendix B to our tutorial)
There isn't much documentation on Mizar; in addition to the
papers at the link above,
A Mizar Mode for HOL by John Harrison is a useful
guide, and also of interest in its own right.
If you are completely new to PVS, the best place to start is with the WIFT Tutorial