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.

Contents 1 Documentation 2 Development 3 Wish List 3.1 Make it easier to use for beginner users 4 News 5 Community 6 Other

Documentation

• FAQ (Frequently Asked Questions)

• PVS API

• Recent Patches

• Building PVS

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
• Fedora package
• Complex number decision package
• Windows Notes

Wish List

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

Make it easier to use for beginner users

There is along discussion about technology transfer of Formal Methods tools, but I personally experienced that still one major blocking factor is the steep learning curve of the tools.

• Windows version: unfortunately still much people use this OS
• Up-to date documentation & tutorials: frustrating to use 8 years old documentation and continuously check the release notes
• Improved user interface: I like emacs, but it is hard to convince eclipse users that PVS’s UI is state-of-art. See RISC ProofNavigator http://www.risc.uni-linz.ac.at/research/formal/software/ProofNavigator/

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

Community

• Projects related to PVS

• Groups using PVS

Here are links to the old PVS Users and Related pages: http://pvs.csl.sri.com/user-links.shtml, and http://pvs.csl.sri.com/links.shtml

Other

We're still learning how best to organize and use this capability--please join in and help.