NASA PVS Library of Formal Developments
Switch branches/tags
Nothing to show
Clone or download
Permalink
Failed to load latest commit information.
ACCoRD Proved all Dec 16, 2017
ASP Fixed some proofs in series. Improved with-fresh-names and with-fresh… Nov 12, 2017
Bernstein Fixed some proofs in series. Improved with-fresh-names and with-fresh… Nov 12, 2017
CCG Fixed some proofs in series. Improved with-fresh-names and with-fresh… Nov 12, 2017
Hypatheon-1.2 Added missing directories Mar 14, 2016
MetiTarski Deprecated trig_fnd. Added trig foundational based on infinite series Jul 15, 2017
PVS0 Updated PVS0 Aug 15, 2018
PVSioChecker Minor changes to PVSioChecker and fast_approx Jul 20, 2018
Riemann Fixed some proofs in series. Improved with-fresh-names and with-fresh… Nov 12, 2017
Sturm Proved all Dec 16, 2017
TRS Fixed some proofs in series. Improved with-fresh-names and with-fresh… Nov 12, 2017
TU_Games Restored .dep files in pvsbin, which were accidentally deleted in the… Jan 31, 2015
Tarski Updates to Hutch May 10, 2018
affine_arith Fixed some proofs in series. Improved with-fresh-names and with-fresh… Nov 12, 2017
algebra ACCoRD May 8, 2015
analysis Fixed some proofs in series. Improved with-fresh-names and with-fresh… Nov 12, 2017
aviation Updated aviation Jan 6, 2018
co_structures Restored .dep files in pvsbin, which were accidentally deleted in the… Jan 31, 2015
complex Proved all Dec 16, 2017
complex_alt Updated complex_alt and complex_integration May 17, 2018
complex_integration Updated complex_alt and complex_integration May 17, 2018
decimals Change PGP key URL in decimals/README.md Mar 19, 2017
digraphs Fixed some proofs in series. Improved with-fresh-names and with-fresh… Nov 12, 2017
docs Renamed docs Apr 3, 2018
exact_real_arith Updated reals, exact_real_arith Sep 20, 2018
examples Proved all Dec 16, 2017
extended_nnreal Restored .dep files in pvsbin, which were accidentally deleted in the… Jan 31, 2015
fast_approx Minor changes to PVSioChecker and fast_approx Jul 20, 2018
fault_tolerance Fixed some proofs in series. Improved with-fresh-names and with-fresh… Nov 12, 2017
float Updated float, interval_arith, and lnexp_fnd for the upcoming version… Nov 27, 2017
graphs Updtaed grand totals Feb 28, 2017
groups Fixed some proofs in series. Improved with-fresh-names and with-fresh… Nov 12, 2017
interval_arith Reproved all developments. Updated summary files Dec 8, 2017
ints Fixed some proofs in series. Improved with-fresh-names and with-fresh… Nov 12, 2017
lebesgue Proved all Dec 16, 2017
linear_algebra Fixed some proofs in series. Improved with-fresh-names and with-fresh… Nov 12, 2017
lnexp_fnd Moved root from lnexp_fnd to power Dec 11, 2017
matrices Fixed some proofs in series. Improved with-fresh-names and with-fresh… Nov 12, 2017
measure_integration Proved all Dec 16, 2017
metric_space Proved all Dec 16, 2017
numbers Fixed some proofs in series. Improved with-fresh-names and with-fresh… Nov 12, 2017
orders Fixed some proofs in series. Improved with-fresh-names and with-fresh… Nov 12, 2017
power Added root_nn to power/root.pvs Dec 12, 2017
probability Proved all Dec 16, 2017
pvs-emacs Emacs patches May 14, 2015
pvs-patches Fixing evalexpr Jul 20, 2018
reals Updated reals, exact_real_arith Sep 20, 2018
scott Restored .dep files in pvsbin, which were accidentally deleted in the… Jan 31, 2015
series Fixed some proofs in series. Improved with-fresh-names and with-fresh… Nov 12, 2017
sets_aux Fixed some proofs in series. Improved with-fresh-names and with-fresh… Nov 12, 2017
sigma_set Restored .dep files in pvsbin, which were accidentally deleted in the… Jan 31, 2015
sorting Updated sorting Apr 5, 2018
structures Updated sorting Apr 5, 2018
summaries Updated reals, exact_real_arith Sep 20, 2018
topology Restored .dep files in pvsbin, which were accidentally deleted in the… Jan 31, 2015
trig Proved all Dec 16, 2017
trig_fnd The library kinematics has been renamed aviation and updated with Pla… Nov 14, 2017
vect_analysis Fixed some proofs in series. Improved with-fresh-names and with-fresh… Nov 12, 2017
vectors Proved all Dec 16, 2017
while Updtaed grand totals Feb 28, 2017
.gitignore Updated README. Fixed minor issues in prove-all, typecheck-all, depen… Feb 17, 2017
CHANGES.txt Updated CHANGES.txt Nov 14, 2017
Hypatheon Added Hypatheon Mar 11, 2016
README.md Update README.md Jul 19, 2018
cleanbin-all Fixed install-scripts and cleanbin-all Oct 20, 2018
dependencygraph Deprecated trig_fnd. Added trig foundational based on infinite series Jul 15, 2017
fetch-hypatheon-db Updated reals,analysis,series Jul 3, 2017
find-all Fixed scripts *-all Dec 12, 2017
install-scripts Fixed install-scripts and cleanbin-all Oct 20, 2018
nasalib-version NASA PVS Library 6.0.9 (Development Version) Oct 27, 2014
nasalib.all Added missing theory to aviation Nov 14, 2017
nasalib.grandtotals Reproved all developments. Updated summary files Dec 8, 2017
nasalib.pdf Added missing theory to aviation Nov 14, 2017
prove-all Moved to2pi properties and to_pi definition from aviation@util and av… Dec 10, 2017
restoredep-all Fixed scripts *-all Dec 12, 2017
typecheck-all Updated README. Fixed minor issues in prove-all, typecheck-all, depen… Feb 17, 2017

README.md

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 http://github.com/nasa/pvslib 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.

Some Pesky Bugs in Recent Versions of Emacs

In recent versions of Emacs, a type-checking error in PVS may result in the Emacs error

error in process filter: let: ‘recenter’ing a window that does not display current-buffer.

After this error, it is necessary to reset PVS. To fix this error, the lines 403 and and 575 in <pvsdir>/emacs/emacs-src/pvs-ilisp.el should be commented out, i.e., they should read

		    ;; (recenter -1)

and

	;; (recenter '(nil))

respectively.

As of Emacs 26.1 (C-h N : view-emacs-news shows the recent changes), the default-major-mode variable was removed. This variable occurs in 2 places in emacs/emacs-src/pvs-ilisp.el. Because of this, PVS displays the following error

error in process filter: Symbol's value as variable is void: default-major-mode

To fix this error, add

 (defvar default-major-mode nil)

to your ~/.emacs or ~/.pvsemacs file.

Enjoy it.

The NASA Langley Formal Methods Team