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.
The purpose of this wiki is to allow more comprehensive and up to date 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.
- FAQ (Frequently Asked Questions)
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
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: For every web development project you need. 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/
- 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
We're still learning how best to organize and use this capability--please join in and help.