FM Program: PVS Developments

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.

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