Home Intro Wiki Docs FAQ Download Bugs Mail FM Tools

PVS Version 2.3

PVS 2.3 is a significant enhancement over PVS 2.2. A large effort has been put into the optimization of several areas of the code and experiments we have performed using a wide variety of specifications have shown impressive speed improvements - if you have examples which show no improvement, or worse a slowdown please send those to us at pvs-bugs@csl.sri.com for analysis.

We tried to make this release backward compatible, but there are syntactic changes that will require changes to the specifications, and other changes, in particular the handling of judgements, that will require adjustments to some proofs. In our validation suite only a small percentage of specifications and proofs needed such adjustments, and in every case the adjustments needed were straightforward. In some cases it helps considerably to run a 2.2 proof side-by-side with a 2.3 proof in order to determine the necessary changes.

The PVS documentation has been fully updated with all of the new features of PVS 2.3. In addition, there is online documentation for some new "experimental features" available at http://pvs.csl.sri.com/experimental/.


The system is available from ftp://pvs.csl.sri.com/pub/pvs/. The file INSTALL in that directory contains the installation instructions. PVS 2.3 is only available for Sun computers running Solaris, and Intel computers running Redhat Linux version 4 or higher.

What's New?

If you have questions or suggestions, send email to pvs-bugs@csl.sri.com.

To get on the PVS mailing list, send a message to pvs-request@csl.sri.com.

Home Intro Wiki Docs FAQ Download Bugs Mail FM Tools

Last modified: Thu 30 Nov 2006 12:15 UTC
Maintainer: Sam Owre