[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

PVS 2.3 patches available




Happy Holidays!

The patches may be obtained from
    http://pvs.csl.sri.com/download.html
or  ftp://pvs.csl.sri.com/pub/pvs/

Get the patch file for your platform; it will be one of:
    pvs-2.3-solaris-patches.tgz
    pvs-2.3-redhat5-patches.tgz
    pvs-2.3-redhat4-patches.tgz
untar them in your top-level PVS 2.3 directory.

This patch is just a bug fix.  Not all known bugs have been fixed,
but some relate to soundness, so we decided to release as soon as
we could get the patches through the validation suite.  In
particular, bugs # 371 and 393 are directly related to soundness,
and it is conceivable that the match bug in # 391 could lead to an
unsoundness, though it is  unlikely.

Although bug # 368 was not really a bug, it pointed to a serious
difficulty in using strings in proofs.  In particular, the decision
procedures know nothing about strings, and their encoding is such that
even the expression "x"="y" cannot be decided.  With this patch, strings
are translated in both the old and new decision procedures as unique
integers.

This patch fixes the following reported bugs:

354: Hendrik Tews - No methods applicable for generic function

355: Joe Stoy - Proofchain incorrectly indicates circular proof

356: Joachim van den Berg - errors when installing PVS 2.3

357: Natarajan Shankar - Abstract-and-mc looks strange

358: "Marcelo & Edith" - assertion BINDINGS failed

359: Antonio Cau - some bugs PVS2.3

360: Natarajan Shankar - Abstract-and-mc old/new decision procedure query

363: Janina Mincer-Daszkiewicz - TYPE FROM int as type of formal parameter

364: Hendrik Tews - formatting long sequences

366: Cesar Munoz - Model-check (Segmentation violation)

367: Jan Friso Groote - Var id 65536 is too large.

368: Peter Homeier - WITH expression does not simplify

370: mokkedem - model-check

371: Mark Lawford - Soundness bug with (inst "epsilon(TRUE)")

372: Hendrik Tews - strange error message

373: Chris George - Overloaded equality in substitutions

374: Cesar Munoz - ground evaluator

380: Mark Aronszajn - A crash to Lisp

381: Geert Pante - Latex: no method applicable
   (Same as 398)

382: Marcelo Glusman - remainder of proof after checkpoint not visible

385: Marcelo Glusman - adding declarations

391: Hanne Gottliebsen - Wrong replace allowed

393: Adriaan de Groot - EXISTS mismatches types

395: Dave Stringer-Calvert - monotonicity tccs

396: Marieke Huisman - escape characters in strings removed

398: Hassen Saidi - Latex generation error.
   (Same as 381)

399: Marieke Huisman - wrong TCC generated

400: Marieke Huisman - Error: the assertion
                       (COMPATIBLE? (TYPE THEN) (TYPE ELSE)) failed. (fwd)

407: Paul Loewenstein - PVS 2.3 Error