| University of Ulm, Faculty of Computer Science, Dept. of Artificial Intelligence | up: PVS @ Ulm |
We maintain a local mirror of the primary PVS distribution site. The information below is copied from there.
Latest version is 3.2
Unless you are a commercial entity, you may freely download PVS, but you must obtain a PVS license. This license covers all existing versions, so you do not need to get a new one to get a new version.
Commercial entities should check their existing license, or contact pvs-licensing@csl.sri.com.
PVS is currently available only for Sparc machines with Solaris 2 and Intel x86 Machines with Linux compatible with Redhat 5 or later. Both of these may reside in the same top-level directory, though different versions must be kept in separate directories.
See the PVS 3.2 Release Notes for a description of the changes.
First get the file(s) you want for the type of machine(s) you have:
Then get the rest of the files
Installation is simple: Create a new PVS directory (name doesn't matter), cd to it, untar the files, run ./bin/relocate, and you should be able to run ./pvs. Copy this script to a directory in your path, or add the PVS directory to your path.
Note: We no longer provide the Emacs 19 files, please upgrade to Emacs or XEmacs 20 or greater. If you really need to run PVS with Emacs 19, contact us at pvs-sri@csl.sri.com
IMPORTANT: If you are running Redhat 9 or equivalent (i.e., with the latest glibc), see the FAQ item PVS problems with Redhat 9 or Enterprise after installing.
PVS 3.1 is currently available only for Sparc machines with Solaris 2 and Intel x86 Machines with Linux compatible with Redhat 5 or later. Both of these may reside in the same top-level directory.
With the exception of commercial entities, if you have an existing license for PVS, you may upgrade to PVS 3.1 without signing a new license. For information on commercial licenses for PVS 3.1, please contact pvs-licensing@csl.sri.com
First get the file(s) you want for the type of machine you have:
Then get the rest of the files
The Release Notes describe the new features.
PVS 3.0 is currently available only for Sparc machines with Solaris 2 and Intel x86 Machines with Linux compatible with Redhat 5 or later. Both of these may reside in the same top-level directory.
With the exception of commercial entities, if you have an existing license for PVS, you may upgrade to PVS 3.0 without signing a new license. For information on commercial licenses for PVS 3.0, please contact pvs-licensing@csl.sri.com
First get the file(s) you want for the type of machine you have:
Then get the rest of the files
The Release Notes describe the new features.
PVS 2.4 is currently available only for Sparc machines with Solaris 2 and Intel x86 Machines with Linux compatible with Redhat 5 or later. Both of these may reside in the same top-level directory.
First get the file(s) you want for the type of machine you have:
Then get the rest of the files
The Release Notes describe the new features.
The files may also be obtained from any of the following mirror sites:
These are automatically updated, but there may be a lag time.
To install, simply create a new directory, cd to it, untar the files, and run ./bin/relocate to set the path. Then run ./pvs, which should start up a new Emacs window running PVS.
After running bin/relocate, the pvs shell script may be copied or linked to a different directory. However, if the PVS directory is moved, ./bin/relocate must be rerun.
If you have already signed a license for PVS, you do not need to sign a fresh one for PVS 3.0. If you obtained the system by anonymous ftp, or by some other means that did not require you to sign the License Agreement beforehand, gunzip and print out the file license.ps.gz, read it, have it signed by someone who can legally bind your institution, and return it to SRI. Licenses are available to individuals as well as corporations and universities.
Earlier versions of PVS are still available:
PVS relies on several other programs being installed on your machine. It is essential that you have Emacs (version 19 or later), and desirable that you have LaTeX, Tcl/Tk.
PVS uses GNU Emacs as its interface; you need Emacs version 19.34 or later to get all the features of PVS; earlier versions of Emacs generally work adequately, but some capabilities will be missing, notably the menus and font-lock support. The Emacs command M-x emacs-version will tell you what version of Emacs you have installed at your site. PVS also works with XEmacs (version 19.13 or later).
Note that PVS 2.4 does not work with Emacs 18. Support for Emacs 19 is available in the file pvs-2.4-emacs19.tgz.
We recommend you install the latest version of GNU Emacs (available from ftp://prep.ai.mit.edu/pub/gnu) or XEmacs (available from ftp://ftp.xemacs.org/pub/xemacs).
Some PVS functions (e.g. proof trees) use Tcl/Tk. For these to work, you must have Tcl/Tk versions 7.3/3.6 or later installed at your site, and the "wish" executable must be on your path You can check this by typing wish at a shell prompt - a little window should pop up - type info tclversion and set tk_version to the % prompt (NOT in the little window) to check the versions. Ctrl-c to exit.
Tcl/Tk is available from ftp://ftp.scriptics.com/pub/tcl/.
LaTeX version 2.09 or 2e is required for typesetting specifications and proofs. Type latex at a shell prompt to make sure LaTeX is available and to see the version number (\bye and x to quit). You'll also need a previewer, which is likely to be called "xdvi".
You can get LaTeX and related software from the Comprehensive TeX Archive Network (CTAN). This is a network of ftp servers rooted at ftp.tex.ac.uk and ftp.dante.de which are widely mirrored and hold up-to-date copies of all the public-domain versions of TeX, LaTeX, Metafont and ancillary programs.
| Dept. of AI Homepage | Research | Help | Mail to Webmaster | H. Pfeifer - last update: Jun 11, 2004 |