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.9 (11/10/14) and
requires PVS 6.0.
For quick installation, follow this instrutions. See installation notes for additional
details. For a list of updates, check
Furthermore, for PVS advanced users, the development version of the NASA PVS Library is available from
The NASA PVS Library is featured in the movie “The Martian”.
- Affine Arithmetic (new):
Formalization of affine arithmetic and strategy for evaluating
polynomial functions with variables on interval domains (examples).
Formalization of multivariate Bernstein polynomials. Note: The strategy
bernstein, which is available in PVS 5.0, has not been
ported to PVS 6.0.
A database capability for PVS theories.
- Interval Arithmetic:
Formalization of interval arithmetic and strategies based on
intrerval analysis (examples
and more examples).
Integration of the theorem prover MetiTarski and SMT solver Z3 as
external oracles to PVS (examples).
Formalization of Sturm's Theorem and strategies for proving
univariate polynomial relations over a real interval (examples).
Formalization of Tarski's Theorem and strategy for proving systems
of univariate polynomial relations on the real line (examples).
- Pre-installed in PVS:
Animation tool of PVS functional specifications (examples).
Previous versions of the NASA PVS Library
identifies links that are outside
the NASA domain