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

PVS 4.1 Release Notes

PVS 4.1 is primarily a bug fix release; there are few new features. Some of the changes do affect proofs, though our experience is that only a few proofs need adjustment, and most of these were quite easy to recognize and fix.

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 the pre-built CMU Lisp image.

The build process is largely untested outside of SRI. The process has been somewhat improved with this release, but please let us know of your experiences, and suggestions for improvement. Problems and solutions may be sent to pvs-bugs@csl.sri.com. If you are more ambitious, feel free to expand on the build description in the PVS Wiki (pvs-wiki.csl.sri.com).

PVS was recently moved from CVS to Subversion, and you can now access the system using svn:

svn checkout https://spartan.csl.sri.com/svn/public/pvs/trunk pvs

For now, this is read-only outside of SRI. If you wish to contribute code to PVS, please send it to pvs-sri@csl.sri.com, and we will assess and incorporate it.



The bugs that have been fixed in 4.1 are mostly those reported since December 2002. Some of these fixes are to the judgement and TCC mechanism, so may have an impact on existing proofs. As usual, if it is not obvious why a proof is failing, it is often easiest to run it in parallel on an earlier version of PVS to see where it differs.

Some of the differences can be quite subtle, for example, one of the proofs that quit working used induct-and-simplify. There were two possible instantiations found in an underlying inst? command, and in version 3.0 one of these led to a nontrivial TCC, so the other was chosen. In version 4.1, a fix to the judgement mechanism meant that the TCC was no longer generated, resulting in a different instantiation. In this case the proof was repaired using :if-match all.

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.