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

The current version of the library is NASA PVS Library 6.0.6 (9/4/13) and requires PVS 6.0. See installation notes for additional details.

An important upgrade of this version of the library is the integration of the automated theorem prover MetiTarski and the SMT solver Z3 as external oracles (in collaboration with William Denman, University of Cambridge, UK). This integration is available through the proof rule `metit`. The basic and classic distributions are "MetiTarski ready", i.e., these distributions include the proof rule `metit`, but the tools MetiTarski and Z3 have to be installed separately for the proof rule to work. On the other hand, the full distribution includes pre-installed binaries of MetiTarski 2.2 and Z3 4.3.1 for Mac OSX 10.7.3 and higher and 64-bits Linux. Please, see METIT-LICENSE.txt and Z3-LICENSE.txt before using these pre-installed binaries.

This version of the library also includes several improvements to `interval_arithmetic`. In particular, it includes support for safe and proper arithmetic operations (as suggested by Gabor Madl, Honeywell, US) and improved strategies for verifying properties on real-valued functions. The strategies handle the basic arithmetic operators (`+,-,*,/`), power (`^`), absolute value (`abs`), square root (`sqrt`), square function (`sq`), trigonometric functions (`sin`, `cos`, `tan`, `atan`), logarithmic and exponential functions (`ln`, `exp`), irrational constants (`pi` and `e`), strict and non-strict inequality operators (`<,<=,>,>=`), interval membership (`##`), interval inclusion (`<<`), Boolean operators (`and`, `or`, `implies`, `not`), conditionals (`IF-THEN-ELSE-ENDIF`), and let-in expressions (`LET-IN`).

Patches and updates since PVS 6.0 include:

• `choice_facts` and `refinement_relations` (thanks to Dragan Stosic).
• `TRS`: added confluence theorem for orthogonal rewriting systems (thanks to Ana Cristina Rocha, Andre Galdino, and Mauricio Ayala, Universidade de Brasilia, Brazil).
• `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).
• `graphs`: Removed `seq_def.pvs` since it duplicates the prelude's type `finseq`. Moved `seq_pidgeon.pvs` to `structures/seq_pigeon.pvs`.
• `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).
• MetiTarski/Z3: 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

The tag identifies links that are outside the NASA domain