SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
  SRI Logo

A Less Elementary Tutorial for the PVS Specification and Verification System
 by Dr. John Rushby & David W.J. Stringer-Calvert.

Number CSL-95-10.
Menlo Park, CA.
June, 1995.


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.

BibTEX Entry
    AUTHOR = {John Rushby and David {W.J.} Stringer-Calvert},
    TITLE = {{A} Less Elementary Tutorial for the {PVS} Specification and Verification System},
    YEAR = {1995},
    NUMBER = {{CSL-95-10}},
    ADDRESS = {Menlo Park, {CA}},
    MONTH = {jun},
    NOTE = {Revised July 1996.},
    URL = {}


About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2024 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy