We provide source, and also pre-built binaries using Allegro Lisp, SBCL, and CMU Lisp, depending on the version. Unless you plan on building the system yourself, or are a commercial entity, we recommend getting the Allegro binaries with the click-through license as it is faster and more thoroughly tested.
Noncommercial entities: you may freely download Allegro runtime versions of PVS, but you must read and accept the "click-through" license that comes up when you choose an allegro download.
Commercial entities: if you have an existing, current PVS license, simply accept the "click-through" license, otherwise first contact us at pvs-licensing@csl.sri.com
Note that CMU Lisp binaries are available starting with PVS 4.0; for earlier versions (and for the Intel Mac version) you must get an Allegro build. Also note that the Allegro versions are faster.
Note that you may get the latest version of the sources using github:
git clone https://github.com/samowre/PVS.git pvs
The following files are a snapshot of the sources used to build the corresponding versions of PVS:
Installation of binaries is simple: Create a new PVS directory (name doesn't matter), cd to it, untar the file(s), run bin/relocate, and you should be able to start PVS with ./pvs. You can then copy this script to a directory in your path, or add the PVS directory to your path. All of the above tarfiles should be untarred in the same directory (but not with different PVS version numbers); just make sure to rerun bin/relocate. Note: there is now only one file needed for installation, it includes the system, binary, and library files.
If you have existing PVS specifications, it's best to make a copy before running them through a newer version of PVS. This makes it easier to repair proofs (comparing proofs side-by-side in different PVS versions), and makes it simpler to revert back to the older version of PVS if for some reason you don't want to move to the new version (please tell us why at pvs-sri@csl.sri.com).
PVS is now open source, under the GNU General Public License (GPL). Informally, this means you can get the sources, and do whatever you want with them, except distribute them with software that is unavailable under a GPL-compatible license. PVS uses a dual license model; if you are interested in alternative licensing terms contact us at pvs-license@csl.sri.com.
In order to make the sources useful in a purely open-source environment, PVS has been ported to CMU Common Lisp, which is also freely available. However, it is currently slower than the Allegro version, so we distribute both. Note that the Intel Mac version is currently only available with Allegro Common Lisp.
PVS sources are currently available as a tarball. See the included INSTALL file or go to pvs-wiki/Building_PVS.
In the future, we will have a subversion repository available so that you can keep up with the bleeding edge of PVS development.
PVS 4 is available for Sparc machines with Solaris 2 or later and Intel x86 Machines with Linux compatible with Redhat 5 or later.
When trying a different version of PVS on existing specifications, it is always a good idea to make a copy first, as there are usually some incompatibilities.
We intend to make all earlier versions of PVS available indefinitely, though as hardware and software moves forward (sideways?) it may become increasingly difficult to get it to run.
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.
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.
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.
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.
Even earlier versions of PVS are still available, though they may have problems on newer platforms.
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 http://www.tcl.tk/.
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 holds up-to-date copies of all the public-domain versions of TeX, LaTeX, Metafont and ancillary programs.