|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|
|Organization / Author||nasa|
|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
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.
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
(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
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.
trig_fnd is now deprecated. It's still provided for
backward compatibility, but it should be replaced by
trig. The new
trig, which used to be axiomatic, is now
foundational. However, in contrast to
definitions are based on infinite series, rather than integrals. This
change considerably reduces the type-checking of theories involving
trigonometric functions. The change from
not have a major impact in your formal developments since names of
definitions and lemmas are the same. However, theory importing may be
The PVS developments
DAIDALUS are now
available as part
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.
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.
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
setenv PVS_LIBRARY_PATH "<pvsdir>/nasalib"
In Borne shell (bash or sh), put this line in either
~/.bashrc or ~/.profile:
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
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
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.
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
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.