Accession Number : ADA326917
Title : PVS Theorem Proving Enhancements.
Descriptive Note : Final rept. 23 Sep 96-24 Mar 97,
Corporate Author : SRI INTERNATIONAL MENLO PARK CA
Personal Author(s) : Shankar, Natarajan
PDF Url : ADA326917
Report Date : JUN 1997
Pagination or Media Count : 9
Abstract : 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.
Descriptors : *COMPUTER PROGRAMMING, *COMPUTER PROGRAM VERIFICATION, COMPUTER LOGIC, CONTROL SEQUENCES.
Subject Categories : Computer Programming and Software
Distribution Statement : APPROVED FOR PUBLIC RELEASE