Projects related to PVS

From SRI PVS
Jump to: navigation, search

Contents

NASA Langley

is one of our sponsors and has many PVS users. They have an extensive set of libraries and extensions available at http://shemesh.larc.nasa.gov/fm/fm-pvs.html

In particular, see (Note: All these extensions are included in PVS 5.0):

PVSio is a PVS package that extends the ground evaluator with a predefined library of imperative programming language features such as side effects, unbounded loops, input/output operations, floating point arithmetic, exception handling, pretty printing, and parsing. The PVSio library is implemented via semantic attachments.

ProofLite is a library package for non-interactive proof scripting in PVS. It allows for a literate proving style in PVS where specification and proof scripts reside in the same file (as it is done in Coq and other proof assistants). ProofLite is also suitable for automatic or batch generation of specifications and proof scripts.

The prover strategy packages, Manip and Field, offer enhanced automation for arithmetic deduction. Manip carries out user-directed manipulation steps. Field works with Manip to achieve higher level simplification. Both packages exploit new 3.0/3.1 features for loading libraries, making installation simpler and more robust.

You may retrieve these libraries directly:

SPIDER

The SPIDER (Scalable Processor-Independent Design for Enhanced Reliability) project at NASA Langley has used PVS to verify a number of SPIDER's protocols. Papers and PVS specifications are available at the SPIDER publications page.

ToolIP

ToolIP: Interoperation and Verification of Tools for Design and Analysis of Cryptographic Protcols - see http://blackforest.stanford.edu/toolip/

TIOA2PVS

Tempo: An set of software tools for modeling, simulation, and verification of timed and hybrid systems - see [1]. The underlying semantics is provided by the timed input/output automaton model. More details about the PVS interface are available at [2]

VAMP

The formal verification of the VAMP CPU was done using PVS 2.3.

Personal tools