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
NASA PVS Release 6.0.4b
The current version of the library is 6.0.4b and requires PVS 6.0.
This version of the library includes several upgrades, e.g.,
The packages Extrategies and Field, which are part of PVS, have been
- Recent patches and updates for PVS 6.0.
- Added for-loops and iterations (
- Added Maybe and Unit types (
- Added a preliminary array theory tailored towards ground evaluation (
- Added a generic branch and bound algorithm (
- Added a type of lists of n elements
- Added arrays to lists functions (
- Added computable finite sets (
(thanks to Pierre Neron from Ecole Polytechnique, France).
digraphs: Revisited several definitions and
lemmas (thanks to Andreia Avelar and Mauricio Ayala-Rincon from
University of Brasilia, Brazil, and Andre Galdino from Federal University of
- Added a formal proofs of Inclusion and Fundamental theorems of interval arithmetic.
- Completely redefined strategies:
interval. These strategies
are now based on computational reflection and are much more efficient than
the previous strategies
packages handle TCCs in a much better way.
Unfortunately, this may cause some strategies to behave in a
slightly way and to break some old proofs.
may generate formulas in a different order. In most cases, the old
skoletin can be simulated by setting the
- Several strategy combinators for building strategies have been
included. Including the possibility to define local strategies
(called tactics), whose scope is the branch of the proof where the
tactic is declared. For a complete list of strategies available in Extrategies and Field, use
the proof commands
The development Bernstein is still missing in this version of the library.
It will be released soon.
A database capability for PVS theories.
Formalization of interval arithmetic and strategies for interval analysis and numerical approximations (examples).
- Pre-installed in PVS:
Previous versions of the NASA PVS Library
The tag identifies links that are outside
the NASA domain