NASA PVS Library
The NASA PVS Library is a collection of formal developments in PVS
maintained by the NASA
Langley Formal Methods Team and is part of the PVS research sponsored by NASA
The current version of the library is NASA PVS Library 6.0.7 (2/28/14) and requires PVS 6.0.
For quick installation instructions, see
README.txt. See installation notes for additional
details. For a list of updates, check
A database capability for PVS theories.
Formalization of Sturm's Theorem and decision procedures for universally and existentially quantified univariate polynomials (examples).
Formalization of interval arithmetic and strategies for interval analysis and numerical approximations (examples
and more examples).
Integration of the theorem prover MetiTarski and SMT solver Z3 as
external oracles to PVS (examples).
- Pre-installed in PVS:
Previous versions of the NASA PVS Library
identifies links that are outside
the NASA domain