If you're having problems using PVS, first try checking the Frequently Asked Questions (FAQ) and then the system manuals. Next, you can try searching the PVS Help archive, or posting a new message to the PVS Help Mailing List, where a body of experienced users can offer help.

The lists of previously reported bugs and suggestions are here:

• Bugs List
• Suggestions List

Reporting Bugs

If you have a problem with PVS that you believe may be due to a bug, there are several steps you can take that will enable us to solve your problem.

Note: we recognize that most users are quite busy and just trying to get their work done, so if you do not have time to go through these steps, just send a quick note describing the bug, along with the specification file(s) that are involved. We will ask for more information if we need it.

Another note: If you are not sure whether you have a bug, report it anyway. If it is due to a misunderstanding, then it means there is a problem in the documentation, and that is still a bug.

If you want to make our job easier, follow the following steps:

• First, search the PVS bug tracking database to see if you've encountered a known problem.
• If your problem is not listed in the currently known bugs, then send (where possible) the following information:
  • A description of the problem, (hopefully minimized) to enable us to reproduce the error.
  • The version of PVS you are using (reported by M-x pvs-version).
  • The version of Emacs you are using (reported by M-x emacs-version).
  • The operating system you are using (reported by uname -a at the shell prompt).
• The information should be sent to us at pvs-bugs@csl.sri.com. Within PVS you can use the command M-x smail-pvs-files to do this and include your specification file(s) automatically.

Note that our bug tracking system is moderated. When you submit a bug the mail message is used to create a problem report under human control. If the specification (or any other information) you are including is confidential or proprietary, we can remove it before entering the problem into the public part our bug tracking database. Just include your request in the beginning of your bug report, or send two separate messages, one to add to the database, and one that includes details of the bug that you would rather not advertise.