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:

• Manip 1.1
• Field.2a

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