• Stars
    star
    186
  • Rank 207,383 (Top 5 %)
  • Language
    Common Lisp
  • Created about 10 years ago
  • Updated about 1 year ago

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

NASA PVS Library of Formal Developments

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

NASALib dependency graph

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 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 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é 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

More Repositories

1

openmct

A web based mission control framework.
JavaScript
11,117
star
2

fprime

F´ - A flight software and embedded systems framework
C++
10,048
star
3

NASA-3D-Resources

Here you'll find a growing collection of 3D models, textures, and images from inside NASA.
Mathematica
2,804
star
4

apod-api

Astronomy Picture of the Day API service
Python
824
star
5

astrobee

NASA Astrobee Robot Software
C++
811
star
6

earthdata-search

Earthdata Search is a web application developed by NASA EOSDIS to enable data discovery, search, comparison, visualization, and access across EOSDIS' Earth Science data holdings.
JavaScript
745
star
7

trick

Trick Simulation Environment. Trick provides a common set of simulation capabilities and utilities to build simulations automatically.
C++
685
star
8

Transform-to-Open-Science

Transformation to Open Science
639
star
9

cFS

The Core Flight System (cFS)
CMake
537
star
10

XPlaneConnect

The X-Plane Communications Toolbox is a research tool used to interact with the X-Plane flight simulator
C
536
star
11

osal

The Core Flight System (cFS) Operating System Abstraction Layer (OSAL)
C
486
star
12

api-docs

api.nasa.gov
SCSS
448
star
13

NASTRAN-95

Fortran
393
star
14

spaceapps

363
star
15

cFE

The Core Flight System (cFS) Core Flight Executive (cFE)
C
343
star
16

instructions

https://github.com/nasa/nasa.github.io/blob/master/docs/INSTRUCTIONS.md
HTML
336
star
17

World-Wind-Java

World Wind, an open source 3D interactive world viewer, was created by NASA's Learning Technologies project, and released in mid-2004. It is now developed by NASA staff and open source community developers.
C++
328
star
18

ogma

Haskell
327
star
19

Common-Metadata-Repository

Clojure
302
star
20

VICAR

291
star
21

CFL3D

Fortran
267
star
22

Open-Source-Catalog

Contains the NASA open source software catalog for automatic deployment to code.nasa.gov
JavaScript
259
star
23

openmct-tutorial

A tutorial for OpenMCT that guides you through integrating historical and realtime telemetry.
JavaScript
242
star
24

code-nasa-gov

code.nasa.gov site leveraging the Open Source Catalog on github.com, powered by Polymer
CSS
236
star
25

eefs

EEPROM File System
C
232
star
26

cumulus

Cumulus Framework + Cumulus API
JavaScript
230
star
27

T-MATS

An open source thermodynamic modeling package completed on behalf of NASA. The Toolbox for the Modeling and Analysis of Thermodynamic Systems (T-MATS) package offers a MATLAB/Simulink toolbox that gives a developer the ability to create simulations of such thermodynamic systems as turbomachinery and gas turbines. Keywords: TMATS, Control System, Numerical Methods, Newton-Raphson, Jacobian Calculation, Propulsion, Aircraft Engine, Jet, Turbofan, Turbojet, Compressor, Turbine, Nozzle, Inlet, open source
HTML
216
star
28

isle

JavaScript
213
star
29

europa

C++
207
star
30

nasa-latex-docs

An easy and convenient package to create technical LaTeX documents.
TeX
197
star
31

delta

Deep Learning for Satellite Imagery
Python
184
star
32

CrisisMappingToolkit

NASA Ames Crisis Mapping Toolkit
Python
183
star
33

nos3

NASA Operational Simulator for Small Satellites
C
167
star
34

icarous

ICAROUS is a software architecture for the development of UAS applications
C
147
star
35

DERT

DERT is an open source software tool for exploring NASA's digital terrain models in 3D
Java
142
star
36

NASTRAN-93

NASTRAN is the NASA Structural Analysis System, a finite element analysis program (FEA)
Fortran
134
star
37

ow_simulator

Python
129
star
38

meshNetwork

C++
127
star
39

prog_models

The NASA Prognostic Model Package is a Python framework focused on defining and building models for prognostics (computation of remaining useful life) of engineering systems, and provides a set of prognostics models for select components developed within this framework, suitable for use in prognostics applications for these components.
122
star
40

QuIP

QuIP provides an interactive environment for computing and presenting images and image sequences, manipulating and storing arbitrary data, and general scientific computing and plotting. The current release supports unix-like operating systems (tested on Linux and Mac OSX), and Apple's iOS mobile operating system. GPU acceleration is supported with either CUDA or OpenCL. There is built-in support for psychophysical experimentation, with general-purpose staircase routines and analysis of psychometric functions.
C
118
star
41

autodoc

Create Microsoft Documents automatically using Text and Template files
106
star
42

Kodiak

Library for rigorous verification of non-linear arithmetic
C++
103
star
43

PrognosticsAlgorithmLibrary

MATLAB
103
star
44

EMIT-Data-Resources

This repository provides guides, short how-tos, and tutorials to help users access and work with data from the Earth Surface Mineral Dust Source Investigation (EMIT) mission.
HTML
102
star
45

CompDam_DGD

Fortran
99
star
46

astrobee_android

NASA Astrobee Robot Software, Android
Java
96
star
47

OpenSPIFe

The Open Scheduling and Planning Interface for Exploration (OpenSPIFe) is an integrated planning and scheduling toolkit based on hundreds of hours of expert observation, use, and refinement of state-of-the-art planning and scheduling technology for several applications within NASA.
Java
95
star
48

HDTN

High-rate Delay Tolerant Network (HDTN) Software
C++
90
star
49

PrognosticsModelLibrary

MATLAB
89
star
50

mmt

NASA's Metadata Management Tool.
Ruby
86
star
51

kepler-pipeline

Kepler Science Data Processing Pipeline
C
84
star
52

IDF

C++
80
star
53

nasapress

A WordPress theme built on the NASA Web Design Standards
PHP
79
star
54

PyTDA

Python Turbulence Detection Algorithm (PyTDA)
Jupyter Notebook
78
star
55

harmony

Application for providing services for Earth observation data in the cloud using standards-based APIs
TypeScript
74
star
56

RHEAS

Regional Hydrologic Extremes Assessment System
Python
73
star
57

astrobot

A slack bot integration with NASA data
JavaScript
73
star
58

podaacpy

A python utility library for interacting with NASA JPL's PO.DAAC
Python
73
star
59

CCDD

CFS Command and Data Dictionary Tool (CCDDT)
Java
72
star
60

SMCPy

Python module for uncertainty quantification using a parallel sequential Monte Carlo sampler
Python
71
star
61

NASA-Acronyms

JavaScript
71
star
62

PointCloudsVR

C++
68
star
63

channel-emulator

C++
66
star
64

cFS-GroundSystem

The Core Flight System (cFS) Ground System Lab Tool (cFS-GroundSystem)
Python
65
star
65

CFS-101

63
star
66

AprilNav

C++
61
star
67

common-mapping-client

CMC is a starter-kit for creating web-based mapping applications
JavaScript
60
star
68

PSP

The Core Flight System (cFS) Platform Support Package (PSP)
C
60
star
69

NASAaccess

NASAaccess is R package that can generate gridded ascii tables of climate (CIMP5) and weather data (GPM, TRMM, GLDAS) needed to drive various hydrological models (e.g., SWAT, VIC, RHESSys, ..etc)
R
60
star
70

CryptoLib

Provide a software-only solution using the CCSDS Space Data Link Security Protocol - Extended Procedures (SDLS-EP) to secure communications between a spacecraft running the core Flight System (cFS) and a ground station.
C
60
star
71

GTM_DesignSim

MATLAB
59
star
72

dictionaries

A collection of NASA "dictionaries", including thesauri, taxonomies and ontologies.
HTML
58
star
73

progpy

The NASA Prognostic Python Packages is a Python framework focused on defining and building models and algorit for prognostics (computation of remaining useful life) of engineering systems, and provides a set of models and algorithms for select components developed within this framework, suitable for use in prognostic applications.
Python
57
star
74

libSPRITE

libSPRITE is a set of libraries that have been used on several past projects including flight, technology demonstration, and simulation projects. libSPRITE provides a diverse set of functions to attempt to simplify coding and reduce code errors. For example, libSPRITE defines engineering units as types (i.e., Meters or Radians instead of double or int). It includes an engineering unit aware math library. libSPRITE includes a task scheduling system that abstracts pthreads and includes a publish subscribe data system for data routing. In addition, libSPRITE includes an optional binding to the Lua scripting language for configuring the program, setting parameters, running Lua scripts within C++ tasks and even interacting with the application during runtime.
C++
57
star
75

prog_algs

The Prognostic Algorithm Package is a python framework for model-based prognostics (computation of remaining useful life) of engineering systems, and provides a set of algorithms for state estimation and prediction, including uncertainty propagation. The algorithms take as inputs prognostic models (from NASA's Prognostics Model Package), and perform estimation and prediction functions. The library allows the rapid development of prognostics solutions for given models of components and systems. Different algorithms can be easily swapped to do comparative studies and evaluations of different algorithms to select the best for the application at hand.
57
star
76

utm-apis

The collection of APIs for NASA's UTM project in the form of OpenAPI documents.
55
star
77

cumulus-dashboard

Cumulus API Dashboard
JavaScript
55
star
78

hybridq

HybridQ is a highly extensible platform designed to provide a common framework to integrate multiple state-of-the-art techniques to simulate large scale quantum circuits on a variety of hardware. HybridQ provides tools to manipulate, develop, and extend noiseless and noisy circuits for different hardware architectures. HybridQ also supports large-scale high-performance computing (HPC) simulations, automatically balancing workload among different processor nodes and enabling the use of multiple backends to maximize parallel efficiency. Everything is then glued together by a simple and expressive language that allows seamless switching from one technique to another as well as from one hardware to the next, without the need to write lengthy translations, thus greatly simplifying the development of new hybrid algorithms and techniques.
Python
55
star
79

pretrained-microscopy-models

Python
54
star
80

GFR

GFR (Glenn Flux Reconstruction) software (LEW-19709-1) has been approved for an open source release
Fortran
54
star
81

refine

C
53
star
82

NASA-Space-Weather-Media-Viewer

Space Weather and the Sun.
52
star
83

giant

Goddard Image Analysis and Navigation Tool
Python
51
star
84

EADINLite

EADIN_Lite Network Protocol
C++
51
star
85

SingleDop

Single Doppler Retrieval Toolkit (SingleDop)
Jupyter Notebook
50
star
86

multipath-tcp-tools

C++
49
star
87

OnAIR

The On-board Artificial Intelligence Research (OnAIR) Platform is a framework that enables AI algorithms written in Python to interact with NASA's cFS. It is intended to explore research concepts in autonomous operations in a simulated environment.
Python
48
star
88

bingo

Python
48
star
89

MMM-Py

Marshall MRMS Mosaic Python Toolkit
Jupyter Notebook
48
star
90

CF

The Core Flight System (cFS) CFDP application.
C
47
star
91

ipv6_python

Python
47
star
92

MLMCPy

Python
47
star
93

TTECTrA

An open source, semi-automated, control design tool for subsonic aircraft engine simulations written in the MATLAB/Simulink environment. The Tool for Turbine Engine Closed-loop Transient Analysis provides the user a preliminary estimate of the closed-loop transient performance of an engine model.
47
star
94

WellClear

Well-Clear Boundary Models for Integration of UAS in the NAS
HTML
46
star
95

CertWare

Java
46
star
96

fpp

F Prime Prime: A modeling language for F Prime
C++
46
star
97

podaac_tools_and_services

A meta-repository which essentially lists code related to all tools and services software for NASA JPL's PO.DAAC
Python
45
star
98

cmr-stac

TypeScript
44
star
99

RtRetrievalFramework

C++
43
star
100

mplStyle

Matplotlib object oriented style system
Python
43
star