Main Page

From SRI PVS

This is the root of the Wiki pages for the PVS Verification System.

The PVS static web pages are at http://pvs.csl.sri.com.

Wikis for our other systems are here: SAL, Yices; and here's our top-level wiki: Formal Methods at SRI CSL.

The purpose of this wiki is to allow more comprehensive and uptodate dissemination of information relating to PVS, and formal methods in general, by allowing anybody to edit these pages. You are encouraged to read and contribute to this wiki. Please make sure your content is relevant to PVS. We are using the MediaWiki software (same as Wikipedia). Click on 'Help' button on the left for using the Wiki.

1 Documentation
2 Development
3 Wish List
4 News
5 Community
6 Other

[edit]

Documentation

FAQ (Frequently Asked Questions)

PVS API

Recent Patches

Building PVS

[edit]

Development

If you are doing some development, porting, or extensions of PVS, add a note here so that others can collaborate, or at least not duplicate effort.

Porting to another Lisp

BDD port to 64-bit

[edit]

Wish List

Add here any new features you would like to see in PVS.

[edit]

News

PVS 4.1 is available at http://pvs.csl.sri.com.

The big news is that with Version 4.0, PVS is (finally!) going open source.
New features in PVS 4.0 include a random tester (like Quickcheck in Haskell) and the ability to use the SMT solver Yices as an endgame prover.

Here's a link to the old PVS Status page: http://pvs.csl.sri.com/status.shtml

[edit]