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
Formalization of multivariate Bernstein polynomials. Note: The strategy
bernstein, which is available in PVS 5.0, is still no
operational in PVS 6.0.
A database capability for PVS theories.
Formalization of interval arithmetic and strategies for numerical approximations and interval 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