Announcing PVS Version 2.2 PVS Version 2.2 is now available. We suggest all PVS users upgrade to this version as soon as possible as we'll be phasing out support for the older versions. PVS 2.2 includes updated documentation, a number of bug fixes, and some new features. It also provides new images for the SunOS, Solaris, and Linux platforms. The new image loads much faster, and uses less memory. We do not currently have a new image for the RS6000/AIX version, but patches are provided that give the full functionality of Version 2.2. (Any AIX users who find this really inconvenient should let us know--if there's enough demand, we'll try to create a new image). The bugs fixed include all the ones marked "feedback" in the pvs-bugs list at http://www.csl.sri.com/htbin/pvs/pvs-bug-list We ran this version against a validation suite with 922 PVS specification files and 5,068 proofs, including those submitted with most of the recent bug reports. Less than 1% of these required modifications to repair the proofs. This was primarily due to bug fixes that cause a different number of TCCs to be generated. In all cases the effort required to repair the proofs was minor. Users who experience real difficulties should please let us know. The updated documents include the System Guide, Language Reference, and Prover Guide. To obtain the system and documentation, connect to our web site at http://www.csl.sri.com/pvs.html or use ftp to access ftp.csl.sri.com:/pub/pvs/ and read the INSTALL file. New Features: + Override (WITH) expressions: a distinction is now made between ordinary override (using :=) and domain extension (using |->). See the Language Reference for details. + decompose-equality: is a new prover strategy that makes it easier to prove, for example, that two record expressions are not equal. See the prover guide for details. + Messages and warnings: warnings and informational messages may be produced as files and theories are processed--e.g., indicating conversions that have been applied. + Works with version 20 of both GNU Emacs and XEmacs. + auto-rewrite!!: An auto-rewrite!! strategy has been added which auto-rewrites non-recursive definitions, even when all the arguments are not available. In addition, the ALWAYS? parameter to the various auto-rewrite strategies may be given as !! to achieve the same effect. + inst?: Now allows a POLARITY? flag for more control over the matching. For example, in R(a,b), FORALL x,y: R(x,y) IMPLIES R(y,x) |- R(b,a) (inst? :polarity? t) will not use the substitution [b/x,a/y]. This argument is also available in the bash, reduce, and grind strategies. + inductive definitions: have been generalized so that if the syntactic monotonicity check fails, a TCC, rather than a typecheck error, is generated. This allows you to attempt to establish monotonicity by proof. + rule-induct: A new strategy is available for inducting over inductive definitions. + Semicolon use: the parser has been modified to allow semicolons after importings, judgement, and conversion declarations. + Renamed whereis-declaration-used to whereis-identifier-used, and added a new whereis-declaration-used function to work on the declaration rather than the string. Adjusted key bindings accordingly. + forward-chain: May now be applied to antecedent formulas. + Proof backups: You may now indicate the number of backups kept for .prf files. 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. We hope you find PVS useful and fun.