NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Collections About News Help Login

Due to the lapse in federal government funding, NASA is not updating this website. We sincerely regret this inconvenience.

Back to Results
Batch Proving and Proof Scripting in PVSThe batch execution modes of PVS are powerful, but highly technical, features of the system that are mostly accessible to expert users. This paper presents a PVS tool, called ProofLite, that extends the theorem prover interface with a batch proving utility and a proof scripting notation. ProofLite enables a semi-literate proving style where specification and proof scripts reside in the same file. The goal of ProofLite is to provide batch proving and proof scripting capabilities to regular, non-expert, users of PVS.
Document ID
20070012333
Acquisition Source
Langley Research Center
Document Type
Contractor Report (CR)
Authors
Munoz, Cesar A. (National Inst. of Aerospace Hampton, VA, United States)
Date Acquired
August 23, 2013
Publication Date
February 1, 2007
Subject Category
Mathematical And Computer Sciences (General)
Report/Patent Number
NIA Report No. 2007-03
NASA/CR-2007-214546
Report Number: NIA Report No. 2007-03
Report Number: NASA/CR-2007-214546
Funding Number(s)
CONTRACT_GRANT: NCC1-02043
WBS: WBS 411931.02.07.07
Distribution Limits
Public
Copyright
Work of the US Gov. Public Use Permitted.

Related Records

There are no records associated with this record.
No Preview Available