[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
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

+ 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.

Sam Owre
Dave Stringer-Calvert