NASA Langley Formal Methods


home

welcome

quick page

philosophy

team

research

quote

links

new?
  home > old > PVS

FM Program: PVS Developments


This page is not maintained. It is probably out of date.

NASA Langley's formal methods program has used PVS (Practical Verification System) external link 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 external link tag identifies links that are outside of the NASA domain.

 

   
home | welcome | quick page | philosophy | team | research | quote | links | new?
Curator and Responsible NASA Official: C. Michael Holloway
larc privacy statement
last modified: 22 May 2001 (08:44:54)