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



We are fighting with a PVS bug in the PVS Version 2.1 (patch level
2.417). We would appreciate any help. 

We have a large specification with several theory files. All lemmas were
proven correct with PVS 2.1 (patch2 version 2.414). If we rerun the
proofs automatically we get 100% of the lemmas proven correct (after
disabling the bin-files). However, if we introduce a change and want to
reprove the lemmas in question, the system breaks.

* In some cases, the prover was actually breaking and PVS had to be
restarted. This serious problem was removed by applying more basic proof

* Continuing with further proofs, the PVS environment seems to exhibit
an inconsitant behavior. Independent of the completeness of a proof, the
proof file is corrupted. In general only some of the proofs of the
theory are stored in the prf-file.  

We are seeking for any kind of advice to overcome these problems. As we
have updated our Emacs version to 20.2.1 we are basically restricted to
patch level 2.417. However, if these problems can not be overcome we
would appreciate to get a hold of the earlier version of PVS 2.1 (patch2
version 2.414). As we are trying to overcome these problems for several
weeks, we would appreciate immediate access to the previous version.

Thank you for your help and we would be glad to receive any immediate

Victoria Chernyakhovsky