John Rushby and David W.J. Stringer-Calvert
Technical Report SRI-CSL-95-10
Abstract
PVS is a verification system that provides a
specification language integrated with support tools and a
theorem-prover. It has been used at SRI and elsewhere to perform
verifications of several significant algorithms (primarily for
fault-tolerance) and large hardware designs. 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.
gzip'd postscript
Directory
of dump files for the Elementary tutorial