Home Intro Wiki Docs FAQ Download Bugs Mail FM Tools

A Less Elementary Tutorial for the PVS Specification and Verification System

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

Home Intro Wiki Docs FAQ Download Bugs Mail FM Tools

Last modified: Fri 22 Mar 2013 17:35 PDT
Maintainer: Sam Owre