NASALib
NASALib is a continuing collaborative effort that has spanned over 3 decades, to aid in research related to theorem proving sponsored by NASA (https://shemesh.larc.nasa.gov/fm/pvs/). It consists of a collection of formal development (i.e., libraries) written in the Prototype Verification System (PVS), contributed by SRI, NASA,NIA, and the PVS community, and maintained by the NASA/NIA Formal Methods Team at LaRC.
Release
The current version of NASALib is 7.1.1 (1/30/23) and requires PVS 7.1.
Libraries
Currently, NASALib consists of 64 libraries, containing about 35K proven formulas.
| Library | Description |
|---|---|
| ACCoRD | Framework for the analysis of air traffic conflict detection and resolution algorithms |
| affine_arith | Formalization of affine arithmetic and strategy for evaluating polynomial functions with variables on interval domains |
| algebra | Groups, monoids, rings, etc |
| analysis | Real analysis, limits, continuity, derivatives, integrals |
| ASP | Denotational semantics of Answer Set Programming |
| aviation | Support definitions and properties for aviation-related formalizations |
| Bernstein | Formalization of multivariate Bernstein polynomials |
| CCG | Formalization of diverse termination criteria |
| complex | Complex numbers |
| complex_alt | Alternative formalization of complex numbers |
| complex_integration | Complex integration |
| co_structures | Sequences of countable length defined as co-algebraic datatypes |
| digraphs | Directed graphs: circuits, maximal subtrees, paths, DAGs |
| dL | Differential Dynamic Logic |
| exact_real_arith | Exact real arithmetic including trig functions |
| examples | Examples of application of the functionality provided by NASALib |
| extended_nnreal | Extended non-negative reals |
| fast_approx | Approximations of standard numerical functions |
| fault_tolerance | Fault tolerance protocols |
| float/axm_bnd | Floating point arithmetic (Axiomatic IEEE-754) |
| float/fnd_bnd | Floating point arithmetic (Foundational generic) |
| float/fnd_unb | Floating point arithmetic (Foundational IEEE-754) |
| float/ieee854 | Floating point arithmetic (Foundational IEEE-854) |
| graphs | Graph theory |
| interval_arith | Interval arithmetic and numerical approximations. Includes automated strategies numerical for computing numerical approximations and interval for checking satisfiability and validity of simply quantified real-valued formulas. This development includes a formalization of Allen interval temporal logic |
| ints | Integer division, gcd, mod, prime factorization, min, max |
| lebesgue | Lebesgue integral with connection to Riemann Integral |
| linear_algebra | Linear algebra |
| line_segments | 2-dimensional line segments |
| lnexp | Logarithm, exponential and hyperbolic functions. & Foundational definitions of logarithm, exponential and hyperbolic functions |
| LTL | Linear Temporal Logic |
| matrices | Executable specification of MxN matrices. This library includes computation of inverse and basic matrix operations such as addition and multiplication |
| measure_integration | Sigma algebras, measures, Fubini-Tonelli Lemmas |
| MetiTarski | Integration of MetiTarski, an automated theorem prover for real-valued functions |
| metric_space | Domains with a distance metric, continuity and uniform continuity |
| mv_analysis | Multivariate real analysis: norms, limits, continuity, derivatives, optimization, etc. |
| mult_poly | Multivariate polynomials and semi-algebriac sets. |
| numbers | Elementary number theory |
| ODEs | Ordinary Differential Equations |
| orders | Abstract orders, lattices, fix points |
| polygons | 2-dimensional polygons |
| polygon_merge | Merge of 2-dimensional polygons without generating holes |
| power | Generalized Power function (without ln/exp) |
| probability | Probability theory |
| PVS0 | Formalization of fundamental computability concepts |
| PVSioChecker | Animation of PVS specifications |
| reals | Summations, sup, inf, sqrt over the reals, absolute value, etc |
| Riemann | Riemann integral |
| scott | Scott topology |
| series | Power series, comparison test, ratio test, Taylor's theorem |
| sets_aux | Power sets, orders, cardinality over infinite sets. Includes functional and relational facts based on Axiom of Choice and refinement relations based on equivalence relations |
| shapes | 2D-Shapes: triangle, parallelogram, rectangle, circular segment |
| sigma_set | Summations over countably infinite sets |
| sorting | Sorting algorithms |
| structures | Bounded arrays, finite sequences, bags, and several other structures |
| Sturm | Formalization of Sturm's theorem for univariate polynomials. Includes strategies sturm and mono-poly for automatically proving univariate polynomial relations over a real interval |
| Tarski | Formalization of Tarski's theorem for univariate polynomials. Includes strategy tarski for automatically proving systems of univariate polynomial relations on the real line |
| topology | Continuity, homeomorphisms, connected and compact spaces, Borel sets/functions |
| trig | Trigonometry: definitions, identities, approximations |
| TRS | Term rewrite systems and Robinson unification algorithm |
| TU_games | Cooperative TU-games |
| vect_analysis | Limits, continuity, and derivatives of vector functions |
| vectors | 2-D, 3-D, 4-D, and n-dimensional vectors |
| while | Semantics for the programming language While |
Structure
Scripts
NASALib also provides a collection of scripts that automates several tasks.
proveit(*) - Runs PVS in batch modeprovethem(*) - Runsproveiton several librariespvsio(*) - Command-line utility to run the PVSio ground evaluator.prove-all- Runsproveiton each library in NASALib by wrappingprovethemin order to provide a specific kind of run.cleanbin-all- Clean.pvscontextand binary files from PVS libraries.find-all- Searches strings matching a given regular expressions in PVS libraries.dependencygraph- Generates a library dependency graph for libraries in the current directory.dependency-all- Generates the dependency graphs for the PVS libraries in the current folder.
Click here for more details on these scripts.
(*) Already included in the PVS 7.1 distribution.
Getting NASALib
Via VSCode-PVS (recommended for new PVS users)
NASALib (v7.0.1) is fully compatible with VSCode-PVS, a modern graphical interface to PVS based on Visual Studio Code. The latest version of NASALib can be installed from VSCode-PVS.
Development Version
For PVS advanced users, the development version is available from GitHub.
To clone the development version, type the following command inside directory where PVS 7.0 is installed. Henceforth, that directory will be referred to as <pvsdir>. In the following commands, the dollar sign
represents the prompt of the operating system.
$ git clone http://github.com/nasa/pvslib nasalib The command above will put a copy of the library in the directory <pvsdir>/nasalib.
Major Recent Changes
-
The library
groupsis now deprecated. Thegrouplibrary was integrated intoalgebra. A symbolic link is still provided for backward compatibility, but its use is discouraged. Every mention togroupsshould be replaced byalgebra. -
The library
trig_fndis now deprecated. It's still provided for backward compatibility, but it should be replaced bytrig. The new librarytrig, which used to be axiomatic, is now foundational. However, in contrast totrig_fnd, trigonometric definitions are based on infinite series, rather than integrals. This change considerably reduces the type-checking of theories involving trigonometric functions. The change fromtrig_fndtotrigshould not have a major impact in your formal developments since names of definitions and lemmas are the same. However, theory importing may be slightly different. -
The PVS developments
TCASII,WellClear, andDAIDALUSare now available as part of the GitHub WellClear distribution. The PVS developmentPRECiSAis now available as part of the GitHub PRECiSA distribution. The PVS developmentPolyCARPis now available as part of the GitHub PolyCARP distribution.
Manual Installation
The following instructions assume that NASALib is located in the directory <pvsdir>/nasalib.
1) Add this directory to the environment variable PVS_LIBRARY_PATH
If it does not exists, creates such variable and with the path of this directory as only content. It is usually very useful to have your shell systems creating this variable at startup. To this end, and depending upon your shell, you may want to add one of the following lines in your startup script. For C shell (csh or tcsh), you may add this line in ~/.cshrc:
setenv PVS_LIBRARY_PATH "<pvsdir>/nasalib"For Borne shell (bash or sh), add this line in either ~/.bashrc or ~/.profile:
export PVS_LIBRARY_PATH="<pvsdir>/nasalib"2) Additional steps to protect previous NASALib configurations (optional)
If you had a previous installation of NASALib, either remove the file ~/.pvs.lisp or, if you have a special configuration in that file, remove the following line
(load "<pvsdir>/nasalib/pvs-patches.lisp") 3) Install Scripts
Finally, go to the directory <pvsdir>/nasalib and run the following shell scripts (the dollar sign represents the prompt of the operating system).
The install-scripts command will update and install NASALib scripts as needed.
$ ./install-scriptsOlder Versions
Older versions of NASALib are available from http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library.
Contributors
NASALib has grown over the years thanks to the contribution of several people, among them:
- Aaron Dutle, NASA, USA
- Alfons Geser, HTWK Leipzig, Germany
- Amer Tahat, Michigan Technological University, USA
- Amy Isvik, Wartburg College, USA
- Ana Cristina Rocha Oliveira, University of Brasilia, Brazil
- AndrΓ© Galdino, Federal University of GoiΓ‘s, Brazil
- Andreia Avelar Borges, University of Brasilia, Brazil
- Anthony Narkawicz, formerly at NASA, USA
- Ariane Alves Almeida, University of Brasilia, Brazil
- Bruno Dutertre, SRI, USA
- Ben Di Vito, NASA (retired), USA
- CΓ©sar MuΓ±oz, formerly at NASA, USA
- ClΓ©ment Blaudeau, EPFL, Switzerland and Ecole Polytechnique, France
- ConcepciΓ³n Vidal, University of La CoruΓ±a, Spain
- David Griffioen,CWI, The Netherlands
- David Lester, Manchester University, UK
- Dragan Stosic, Ireland
- Γrik Martin-Dorel, U. Montpellier 2 & U. of Perpignan (formerly), France
- Esther Conrad, NASA, USA
- Felicidad Aguado, University of La CoruΓ±a, Spain
- Flavio L.C. de Moura, University of Brasilia, Brazil
- Gilles Dowek, INRIA, France
- George Hagen, NASA, USA
- Gilberto Perez, University of La CoruΓ±a, Spain
- Gregory Anderson, University of Texas at Austin, USA
- Hanne Gottliebsen, formerly at NIA, USA
- Heber Herencia-Zapana, formerly at NIA, USA
- J. Tanner Slagel, NASA, USA
- Jerry James, Utah State University, USA
- Jeff Maddalon, NASA, USA
- Jon Sjogren, Department of Defense, USA
- John Siratt, formerly at University of Arkansas at Little Rock, USA
- Katherine Cordwell, CMU, USA
- Kristin Rozier, formerly at NASA, USA
- Laura Titolo, NIA & NASA, USA
- Lee Pike, formerly at Galois, USA
- Marco A. FeliΓΊ, NIA, USA
- Mariano Moscato, NIA, USA
- Mauricio Ayala-RincΓ³n, University of Brasilia, Brazil
- Natarajan Shankar, SRI, USA
- Pablo Ascariz, formerly at University of La CoruΓ±a, Spain
- Paul Miner, NASA, USA
- Pedro Cabalar, University of La CoruΓ±a, Spain
- Radu Siminiceanu, formerly at NIA, USA
- Ricky Butler, NASA (retired), USA
- Silvie Boldo, INRIA, France
- Sam Owre, SRI, USA
- Thaynara de Lima, Federal University of GoiΓ‘s, Brazil
- Thiago Mendonça Ferreira Ramos, University of Brasilia, Brazil
- Thomas Norris
- VΓctor CarreΓ±o, NASA (retired), USA
If we have incorrectly attributed a PVS development or you have contributed to NASALib and your name is not included here, please let us know.
If you want to contribute please read this guide.
DISCLAIMER
NASALib is a collection of formal specifications most of
which have been in the public domain for several years. The Formal
Methods Team at NASA LaRC still
maintains these developments. For the developments originally made by
the Formal Methods Team, these
developments are considered fundamental research that do not
constitute software. Contributions made by others may have particular
licenses, which are listed in the file top.pvs in each
respective directory. In case of doubt, please contact the developers
of each contribution, which are also listed in that file.
PVS patches, which are included in the directory pvs-patches, are part of the
PVS source code and they are covered by the PVS open source license.
Some proof strategies require third party research tools, e.g., MetiTarski and Z3. For convenience, they are included in this repository with permission from their authors. Licenses for these tools are also included as appropriate.
Enjoy it.
The NASA/NIA Formal Methods Team at LaRC
Contact: Mariano Moscato