NASA Langley PVS Libraries

What's New?
Installation Notes
Download

Last Update: March 6, 2008 (Version 5.2)

Although the libraries and strategies are listed separately for documentation purposes, it is recommended that you install all of them together. See installation notes .
LIST OF PVS LIBRARIES
algebra groups, monoids, rings, etc details
analysis§ real analysis, limits, continuity, derivatives, integrals details
calculus§ axiomatic version of calculus details
complex§ complex numbers details
co_structures§ sequences of countable length defined as coalgebra datatypes details
digraphs directed graphs: circuits, maximal subtrees, paths, dags details
float§ floating point numbers and arithmetic details
graphs graph theory: connectedness, walks, trees, Menger's Theorem details
ints integer division, gcd, mod, prime factorization, min, max details
interval interval bounds and numerical approximations details
lnexp§ logarithm, exponential and hyperbolic functions details
lnexp_fnd§ foundational definitions of logarithm, exponential and hyperbolic functions details
orders§ abstract orders, lattices, fixedpoints details
reals§ summations, sup, inf, sqrt over the reals, abs lemmas details
scott§ Theories for reasoning about compiler correctness details
series§ power series, comparison test, ratio test, Taylor's theorem details
sets_aux powersets, orders, cardinality over infinite sets details
sigma_set§ summations over countably infinite sets details
structures§ bounded arrays, finite sequences and bags details
topology§ continuity, homeomorphisms, connected and compact spaces, Borel sets/functions details
trig§ trigonometry: definitions, identities, approximations details
trig_fnd§ foundational development of trigonometry: proofs of trig axioms details
vectors§ basic properties of vectors details
while§ Semantics for the Programming Language "while" details

§ indicates that the library uses the Manip/Field strategies.

See Major Theorems Proved for an index into NASA PVS libraries.

STRATEGIES and Bench Marks
Name Download Concept
Manip PVS3.1 or PVS3.2 algebraic manipulation of formulas ( examples)
Field PVS 3.1 or PVS3.2 remove divisions from a formula
PVSio PVS 3.1 or PVS3.2 enhance PVS simulation capabilities
Test Probs PVS3.1 or PVS3.2 theorem prover benchmark problems ( taunt )


All of the libraries can be retrieved from the following tar files:

PVS4.1 tar file           contains Manip, Field and PVSio       
PVS4.0 tar file           contains Manip, Field and PVSio       
PVS3.3 tar file     
PVS3.2 tar file          
PVS3.1 tar file
PVS2.4 tar file

Installation Notes

To faciliate cooperation we are now providing a UNDER_DEVELOPMENT--tar file containing libraries that are currently under development. Hopefully this we prevent duplication of effort. If you would like to have your incomplete libraries hosted here send them to us.

See PVS Theorem Prover Related Research for NASA Langley sponsored papers on PVS development.

Note: The link to external site tag identifies links that are outside of the NASA domain.

Curator and Responsible NASA Official: Ricky W. Butler
larc privacy statement
last modified: 29 February 2008