PVS Status
- November 22, 2006: PVS 4.0 (open source)
released
-
PVS 4.0 is available, see the download page for details.
- November 21, 2006: PVS Wiki
-
There is now a PVS Wiki
available, based on Mediawiki.
- November 4, 2005: Release of ProofLite
2.a
-
ProofLite is a tool for non-interactive proof checking in PVS. It also
enables a semi-literate proving style where specifications and proof
scripts reside in the same file (as it is done in Coq and other proof
assistants).
ProofLite-2.a is much faster than previous versions and it has new
features:
- Batch generation of proof-traces
- Extraction of ProofLite scripts from proofs
ProofLite is freely available at http://research.nianet.org/~munoz/ProofLite/
Send comments and user reports to César Muñoz.
- 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.
-
Note: PVSio is now included with PVS 4.0
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.
- December 19, 2002: PVS 3.0
released.
-
See the release notes
for details, and go to the download
page to get the new image and documentation.
- July 20, 2002: PVS 3.0 Beta
released.
-
See the release notes
for details, and go to the download
page to get the new image and documentation.
- December 18, 2001: PVS 2.4 patchlevel 1
released.
-
See the release notes
for details, and go to the download
page to get the new image and documentation.
- November 25, 2001: PVS 2.4
released.
-
See the release notes
for details, and go to the download
page to get the new image and documentation.
- September 4, 1999: PVS 2.3
released.
-
See the release notes
for details, and go to the download
page to get the image and documentation.
- February 12, 1999: PVS User Group Meeting and Tutorial at
FM99.
-
There will be a PVS User Group Meeting and Tutorial at FM99. For
more details see the FM 99 Web Site
and the PVS meeting page.
- October 26, 1998: Suggestions page.
-
A new web page has been added to archive suggestions for
improvement and requests for enhanced capability. Follow the link
on the PVS home page or go directly to the suggestions page.
Last modified: Thu 30 Nov 2006 12:15 UTC
Maintainer: Sam Owre