[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

PVS 5.0 Release Notes

PVS 5.0 is a significant new release of PVS. The highlights include an SBCL port, the incorporation of the PVSio, Manip, Field, and ProofLite packages from NASA, a new theory interpretation implementation, new judgement forms, new support for Yices, and several bug fixes.

Installation Notes

The system is installed as usual; see the download pages at


We strongly suggest getting a pre-built Allegro version, unless you have concerns with the Allegro runtime click-though license, in which case get one of the pre-built CMU or SBCL Lisp images.

Note that we are no longer providing PVS for Solaris or PowerPC on the download page, as we have limited funds and the vast majority of our users have Intel Macs or Linux machines. If you do need either of these, let us know at pvs-sri@csl.sri.com. We will be keeping earlier versions available for the foreseeable future.

It’s important to note that the .prf format has changed. While PVS 5.0 can easily read earlier proof files, the new format will confuse earlier versions of PVS. Please make copies of any directories that you want to also use earlier versions of PVS on. This is especially helpful when trying to repair proofs that work in earlier versions.

New Features

Available Lisp/Platforms

There are now 64-bit and 32-bit versions available for Intel Mac and Linux for Allegro (version 8.2) and SBCL Common Lisp. 32-bit versions are also available for CMU Common Lisp.

PVS Invocation

The pvs shell script has been modified to support SBCL Common Lisp. In addition, the load and eval capabilities have been simplified, where -l and -e are for Emacs files and expressions, and -L and -E are for Common Lisp files. There was an earlier -L flag, but it loaded the file before PVS initialization, which is more difficult to use.

PVSio Integration

César Muñoz has provided further improvements for PVSio, which is now more fully integrated into PVS. PVSio provides

PVSio now starts up without the need for loading extra library files. The sematic attachments are pre-installed, and the supporting theories are in the prelude. For more details on how to use PVSio, see the manual in doc/PVSio-2.d.pdf, (but ignore the installation instructions).

Manip and Field

The NASA Manip and Field packages have similarly been integrated, and improved by their authors. The Manip package provides many features, including Emacs extensions, many new proof strategies, and a pattern matching facility that allows reference to subterms during proof. For more details, see doc/manip-guide.pdf (but ignore the install instructions).

The Field package builds on Manip, and adds several prover commands making it easier to reason about nonlinear formulas. See doc/extrategies.pdf for details.


César Muñoz has also provided his ProofLite extension as part of PVS. This allows proofs to be included directly in PVS specifications and run from them, allowing for a literate programming style of specification. See doc/ProofLite-4.2.pdf for details.

Theory Interpretations

Theory interpretations have been significantly modified. Previously a theory declaration would generate a separate theory. This caused all kinds of problems, as it couldn’t reference any declarations from the referencing theory. In some cases this could be handled by splitting theories into pieces, but even this doesn’t always work.

In the new treatment, theory declarations are simply expanded in place, with the theory declaration id prepended to the included theory declarations. This solves the problem with declaration references, but introduces new issues. First, since the expanded theory declaration may itself have theory declarations, names have been extended to include any number of periods, e.g., th1.th2.th3.d. In general, these are only needed to disambiguate, and even then a suffix of the full name usually suffices.

The prettyprint-theory-instance is no longer meaningful, simply use M-x prettyprint-expanded to see the included declarations.

Expression Judgements

A new Judgement form is available. This is still in the experimental stage, but we welcome any feedback. The judgement has the form of a subtype judgement, but with a preceding FORALL that gives the types of the variables, as well as making the parsing unambiguous. Within the forall, any expression is allowed. For example,

 judgement forall (x: real) = x*x has_type nnreal
 f: [nnreal -> real]
 foo: formula forall (y: real):
   f(f((y - 100) * (y - 100)) * f((y - 100) * (y - 100))) = 2

Without the judgement, foo generates 2 TCCs; with the judgement, none are generated for foo, just the one for the judgement itself, which is much simpler to understand. Note that the judgement mechanism has to be fast, and not itself generate proof obligations, so the matches are purely syntactic. Thus ‘(x - 1) * (-1 + x)‘ will still generate a TCC.

Yices Enhancements

There are improvements to the yices and yices-with-rewrites rules. Note that to use these commands you must install Yices from yices.csl.sri.com, and make certain the directory containing the yices executable is in your PATH environment variable before invoking PVS.

PVS Libraries Speedbar

A simple Emacs speedbar extension is now available. This makes browsing libraries easier, as it lists all directories on the PVS_LIBRARY_PATH as well as the built-in libraries in the PVS lib subdirectory. This is invoked with M-x pvs-speedbar-browser, and clicking on a given library shows the specification files within; clicking on one of them brings it up in an Emacs buffer. In the future we plan to include declaration lists within the speedbar display.


The changes lead to some incompatibilities, primarily in the proofs. This is due to a number of factors:

Most of the other incompatibilities are more obvious, and the proofs are easily repaired. If you have difficulties understanding why a proof has failed, or want help fixing it, send it to PVS bugs pvs-bugs@csl.sri.com.

[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

This document was generated by Sam Owre on February 11, 2013 using texi2html 1.82.