Recent announcements are posted here, a complete list, including future
plans are on the Status page.
- November 21, 2006: PVS 4.0 (open source) released -
PVS 4.0 is available, see the download page for details.
- May 24-27, 2005:
NASA Langley - NIA training course on PVS
The Formal Methods teams at NASA Langley Research Center and the
National Institute of Aerospace are offering a short course on
PVS in the spring of 2005. The class will take place May 24-27 in
Hampton, Virginia. We have conducted this course several times in the
past, most recently in April 2003. Our policy is to offer the course
free of charge as a public service to the technical community. In
return, attendees bear the cost of traveling to our site. The class is
open to all interested individuals, including non-US citizens. See the
link above for details and registration information.
- November 29, 2004: Release of PVSio.2a.
PVSio is a PVS package that extends the ground evaluator with a
predefined library of imperative programming language features such as
side effects, unbounded loops, input/output operations, floating point
arithmetic, exception handling, pretty printing, and parsing. The PVSio
library is implemented via semantic attachments.
PVSio is freely available at http://research.nianet.org/~munoz/PVSio/
Send comments and user reports to César Muñoz.
- November 10, 2004: NASA PVS libraries for PVS 3.2.
The NASA PVS libraries have been updated to PVS 3.2. This consists of
the libraries algebra, analysis, calculus,
complex, digraphs, fixedpoints, graphs,
ints, lnexp, number_theory, reals,
series, sets_aux, structures, trig,
trig_fnd, and vectors.
They are freely available at
http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/pvslib.html
or directly from
http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/p32_pvslib-full.tgz
Send comments and user reports to Rick Butler
- November 4, 2004: PVS 3.2 released.
See the download page for details.
- January 9, 2004: ProofLite Package for PVS 3.1.
ProofLite is a library package for non-interactive proof scripting in
PVS. It allows for a literary proving style in PVS where specification
and proof scripts reside in the same file (as it is done in Coq and
other proof assistants). ProofLite is also suitable for automatic or
batch generation of specifications and proof scripts.
ProofLite is freely available at:
http://research.nianet.org/~munoz/ProofLite/
Send comments and user reports to César Muñoz.
- February 18, 2003: Manip 1.1 and Field.2a.
The prover strategy packages, Manip and Field, are now available for PVS
3.1. Both offer enhanced automation for arithmetic deduction. Manip
carries out user-directed manipulation steps. Field works with Manip to
achieve higher level simplification. Both packages exploit new 3.0/3.1
features for loading libraries, making installation simpler and more
robust.
You may retrieve these libraries directly:
Send comments and user reports to Ben Di Vito and César Muñoz.
- February 14, 2003: PVS 3.1 released.
See the announcement
for details, and go to the download
page to get the new image and documentation.