Projects related to PVS

Jump to: navigation, search


NASA Langley

is one of our sponsors and has many PVS users. They have an extensive set of libraries and extensions available at

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:


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: Interoperation and Verification of Tools for Design and Analysis of Cryptographic Protcols - see


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]


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

Personal tools