FM Program: PVS Developments

(Note: most of the following text comes directly from the June 2000 edition of NASA Langley's Research and Technology-Transfer Program in Formal Methods, which is available in PDF and PostScript formats.)

NASA Langley's formal methods program has used PVS (Practical Verification System) developed by SRI International extensively. We have found the tool to be capable, but have also desired improvements.

Currently NASA Langley is funding SRI to develop an interactive simplifier for PVS and a mechanization for theory interpretations. The developed mechanization will make it possible to show that one collection of theories is correctly interpreted by another collection of theories under a user-specified interpretation.

We have also supported the development of abstract datatypes in PVS and the formal sematics for the specification language. Also, in 1996, we sponsored the development of a tabular notation for PVS. We also supported the development of the PVS validation suite and funded a task to develop an approach for efficient direct execution of PVS specifications that can help users validate their specification through exploration of its behavior on test cases or symbolic execution.

Search the Langley Technical Report Server for papers related to this work, and our uses of PVS.

Note: The tag identifies links that are outside of the NASA domain.