DID YOU KNOW? DTIC has over 3.5 million final reports on DoD funded research, development, test, and evaluation activities available to our registered users. Click HERE
to register or log in.
PVS Theorem Proving Enhancements.
Final rept. 23 Sep 96-24 Mar 97,
SRI INTERNATIONAL MENLO PARK CA
Pagination or Media Count:
The goal of the project was to augment PVS with features that simplified the construction and management of proofs, and to document the PVS functions needed for writing proof strategies. The extensions to PVS developed in this project include 1 Multiple-proof maintenance, 2 Comments in proofs, 3 Labeling and accessing sequent formulas, 4 Rerunning proofs with checkpoints, 5 Deconstructing EXPAND, and 6 Saved SKIP command.
APPROVED FOR PUBLIC RELEASE