[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
PVS Version 2.2 now available
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
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
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
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.
+ 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
+ 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
+ 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
If you have questions or suggestions, send email to
To get on the PVS mailing list, send a message to
We hope you find PVS useful and fun.