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., <i>libraries</i>) 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 branch master points to the current development pre-release of NASALib for PVS8.0. The release NASALib v7.1.1 is the final stable release for 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_ax | Axiomatic 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 |

Strategies

NASALib provides several proof producing strategies and oracles.

Proof Producing Strategies in NASALib

| Strategy | Description | Requirements | More Information | | --- | --- | --- | --- | |affine, aa-numerical | Evaluation of multivariate polynomials with variables on interval domains | affine_arith@strategies | Affine| |bernstein | Multivariate polynomial global optimization using Bernstein polynomials | Bernstein@strategies | Bernstein| |interval, numerical | Reasoning about real-valued expression using interval arithmetic | interval_arith@strategies | Interval| |era_numerical | Evaluation of real-valued expressions using exact real arithmetic | exact_real_arith@strategies | examples | |riemann | Numerical integration | Riemann@strategies | examples | |simplify-nth | Simplification of expressions of the form nth((:a0,...,an:),k) to ak when k <=n| | | |sturm| Reasoning about univariate polynomial relations over a real interval | Sturm@strategies | Sturm| |tarski| Proving systems of univariate polynomial relations on the real line | Sturm@strategies | Tarski|

Oracles in NASALib

| Oracle | Description | Requirements | More Information | | --- | --- | --- | --- | |metit | Oracle for real-valued functions | | MetiTarski|

Strategy Packages Included in PVS

| Strategy Package | Description | | --- | --- | | Manip | Strategies aimed at algebraic simplification of real-valued expressions, including syntax-matching and extended reference notations| | Field | Strategies for simplifications and algebraic manipulations in the closed field of real numbers| | Extrategies | Strategy combinators and Lisp functions for writing and debugging PVS strategies|

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 `p