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 Formal Methods Team at LaRC.

Release

The current version of NASALib is 7.1.2 (2023/09/01) and requires PVS 7.1.

Libraries

Currently, NASALib consists of 62 top-level libraries, containing about 38K proven formulas in total.

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	Floating point arithmetic
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.
nominal	Nominal equational reasoning
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
pvsio_utils	Additions to PVSio, a PVS standard library for 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 mode
• provethem (*) - Runs proveit on several libraries
• pvsio (*) - Command-line utility to run the PVSio ground evaluator.
• prove-all - Runs proveit on each library in NASALib by wrapping provethem in order to provide a specific kind of run.
• cleanbin-all - Clean .pvscontext and 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 https://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 groups is now deprecated. The group library was integrated into algebra . A symbolic link is still provided for backward compatibility, but its use is discouraged. Every mention to groups should be replaced by algebra.

• The library trig_fnd is now deprecated. It's still provided for backward compatibility, but it should be replaced by trig. The new library trig, which used to be axiomatic, is now foundational. However, in contrast to trig_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 from trig_fnd to trig should 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, and DAIDALUS are now available as part of the GitHub WellClear distribution. The PVS development PRECiSA is now available as part of the GitHub PRECiSA distribution. The PVS development PolyCARP is 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-scripts

Older 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é Luiz Galdino, Federal University of Catalão, 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
• Ben Hocking, Dependable Computing, USA
• César Muñoz, 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
• Gabriel Ferreira Silva, 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, AMA Inc. & NASA, USA
• Lee Pike, formerly at NASA, USA
• Marco A. Feliú, AMA Inc., USA
• Mariano Moscato, AMA Inc., USA
• Mauricio Ayala-Rincón, University of Brasilia, Brazil
• Natarajan Shankar, SRI, USA
• Pablo Ascariz, formerly at University of La Coruña, Spain
• Paolo Masci, AMA Inc. & NASA, USA
• 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 Arielly 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
• Washington Luis Ribeiro de Carvalho Segundo, University of Brasília, Brazil

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 Formal Methods Team at LaRC

Maintainers

César Muñoz Mariano Moscato