System Requirements

PVS is available for Linux/Intel and Solaris/Sparc. It requires a recent version of xemacs or emacs. If you use a Windows machine, I recommend using a Windows X-Server such as X-Win and X11 connection forwarding from a supported architecture. Contact help@cs if you need help with that, or if you need to install X-Win.

Using PVS from AFS

The easiest way to run PVS is to use the pre-installed version from AFS. In order to run PVS, create a new directory, which will be used to store your theories and proofs. Change into this directory. Then type

/afs/cs.cmu.edu/project/modck-5/pvs_3.1/pvs

Let us know if you have problems accessing this file, or running PVS from this installation.

Your own PVS installation

If you prefer to make your own installation of PVS, get the following files:

1. First get the file for the type of machine you have:

   • pvs-3.1-linux.tgz (Linux)
   • pvs-3.1-solaris.tgz (Solaris)

   Then get the rest of the files

   • pvs-3.1-system.tgz
   • pvs-3.1-emacs19.tgz (Optional - support for [X]Emacs 19)
   • pvs-3.1-libraries.tgz (Optional - libraries)

   The files are available locally via AFS in the directory

   /afs/cs.cmu.edu/project/modck-5/pvs_3.1/pvs

   or directly from the SRI at http://pvs.csl.sri.com/download.html.

2. Second, create a directory for PVS, and change into this directory.

3. Third, un-tar the files with

   tar xfz file.tgz

4. Run

   bin/relocate