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 Langley.

NASA PVS Release 6.0.4b

The current version of the library is 6.0.4b and requires PVS 6.0.

• Basic distribution only includes specification and proof files.
• Classic distribution includes basic distribution and binary files.
• Full distribution includes classic distribution and Hypatheon database utility.
• Installation notes.
• Library content and dependency graph.

This version of the library includes several upgrades, e.g.,

• Recent patches and updates for PVS 6.0.
• structures:
  • Added for-loops and iterations (for_iterate, for_examples).
  • Added Maybe and Unit types (Maybe, Unit).
  • Added a preliminary array theory tailored towards ground evaluation (arrays).
  • Added a generic branch and bound algorithm (branch_and_bound).
  • Added a type of lists of n elements (listn).
  • Added arrays to lists functions (array2list).
  • Added computable finite sets (set_as_list) (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 Goias, Brazil).
• interval_arith:
  • Added a formal proofs of Inclusion and Fundamental theorems of interval arithmetic.
  • Completely redefined strategies: numerical and interval. These strategies are now based on computational reflection and are much more efficient than the previous strategies numerical and instint.
• The packages Extrategies and Field, which are part of PVS, have been completely revisited.
  • These 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. In particular, skoletin may generate formulas in a different order. In most cases, the old behavior of skoletin can be simulated by setting the option :old? to t.
  • 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 extrategies-about and field-about.

The development Bernstein is still missing in this version of the library. It will be released soon.

PVS Utilities

• Hypatheon: A database capability for PVS theories.
• Interval: Formalization of interval arithmetic and strategies for interval analysis and numerical approximations (examples).
• Pre-installed in PVS:
  • Manip: Algebraic manipulation of formulas (examples).
  • Field: Simplification strategies for the field of real numbers (examples).
  • Extrategies: The missing strategies in PVS (examples).
  • PVSio: Animation tool of PVS functional specifications (examples).
  • ProofLite: Batch-proving and proof-scripting tool (examples).

Previous versions of the NASA PVS Library

• For PVS 5.0 (including binaries, excluding binaries, installation notes).
• For PVS 4.2, PVS 4.1, PVS 4.0, PVS 3.3, PVS 3.2, PVS 3.1 (installation notes).

The tag identifies links that are outside the NASA domain