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

PVS 4.2 Release Notes

PVS 4.2 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 are 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 changes lead to some incompatibilities. The improved judgements and TCC subsumption lead to fewer TCCs, hence may cause TCC renumbering and proofs may have to be shifted (M-x show-orphaned-proofs may be useful here).

In addition to these, the improved auto-rewrites also affect proofs, as some branches of a proof may no longer be generated, or may have a different form. It is usually easy to repair, though it often helps to run an older version of PVS in parallel to figure out where the proof deviates. Finally, any proof that relies on the expansion of the will need to use the_lem instead.

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

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