Technology moves fast! ⚡ Don't get left behind.🚶 Subscribe to our mailing list to keep up with latest and greatest in open source projects! 🏆

Subscribe to our mailing list


NASA PVS Library of Formal Developments

Subscribe to updates I use pvslib

Statistics on pvslib

Number of watchers on Github 79
Number of open issues 0
Main language Common Lisp
Average time to merge a PR 1 day
Open pull requests 0+
Closed pull requests 0+
Last commit over 1 year ago
Repo Created over 4 years ago
Repo Last Updated over 1 year ago
Size 40.5 MB
Organization / Authornasa
Page Updated
Do you use pvslib? Leave a review!
View pvslib activity
View on github
Fresh, new opensource launches 🚀🚀🚀
Trendy new open source projects in your inbox! View examples

Subscribe to our mailing list

Evaluating pvslib for your project? Score Explanation
Commits Score (?)
Issues & PR Score (?)

NASA PVS Library

The NASA PVS Library is a collection of formal PVS developments maintained by the NASA Langley Formal Methods Team. The NASA PVS library is part of the research on theorem proving sponsored by NASA Langley.

The current version of the library is NASA PVS Library 6.0.10 (xx/xx/xx) and requires PVS 6.0. The following instructions assume that PVS 6.0 is installed in the directory <pvsdir>, i.e., in the instructions below replace <pvsdir> by the absolute path where PVS is installed.

Getting the Development Version

For PVS advanced users, the development version of the NASA PVS Library is available from GitHub. To clone the development version, type the following command from the directory <pvsdir> (the dollar sign represents the prompt of the operating system).

$ git clone nasalib 

The command above will put a copy of the library in the directory <pvsdir>/nasalib.

This version of the NASA PVS Library includes Hypatheon. Hypatheon is a database utility that provides a capability for indexing PVS theories and making them searchable via a GUI client.

Recent Changes

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.

Getting the Most Stable Version

The most stable version of the NASA Library is available from the NASA PVS Library web site. It comes in 3 sizes: basic, classic, and full. All the distribution files include the same PVS specification and proof files. They differ in the binary files, which are only included in the classic and full distributions. The full distribution also includes pre-installed versions of Z3 and MetiTarski.

Installing the NASA PVS Library

The following instructions assume that the NASA PVS Library is located in the directory <pvsdir>/nasalib. First, set the environment variable PVS_LIBRARY_PATH such that it point to this directory. Depending upon your shell, put one of the following lines in your startup script. In C shell (csh or tcsh), put this line in ~/.cshrc:

setenv PVS_LIBRARY_PATH "<pvsdir>/nasalib"

In Borne shell (bash or sh), put this line in either ~/.bashrc or ~/.profile:

export PVS_LIBRARY_PATH="<pvsdir>/nasalib"

If you had a previous installation of the NASA PVS Library, 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") 

Finally, go to the directory <pvsdir>/nasalib and run the shell script (the dollar sign represents the prompt of the operating system).

$ ./install-scripts
$ ./fetch-hypatheon-db

The former command installs an updated version of pvsio and proveit. The later command fetches an updated version of the NASA PVS Library database to be used by Hypatheon.

For more information visit the installation page.

A Note on Library Terminology

For various reasons, the term PVS library has undergone some evolution. The original meaning is a named collection of related PVS theories all residing within a single directory. Recent usage refers to the NASA PVS Library as a collection of formal developments, where each formal development is realized by a collection of theories. This newer usage places Library at a higher level. Hypatheon, though, was developed with the original library meaning and has retained that terminology. Please be mindful that two variants of the term exist. In the following, we distinguish the newer usage using capitalization. Elsewhere, context should suffice to discern which meaning applies.

Enjoy it.

The NASA Langley Formal Methods Team

pvslib list of languages used
Other projects in Common Lisp