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

Report Date:

1997-06-01

Pagination or Media Count:

9.0

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