[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