Home Intro Wiki Docs FAQ Download Bugs Mail FM Tools

PVS Download and Installation

Latest version is 6.0 - see release notes for details.

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.


PVS Allegro Lisp Binaries (free, but requires a license agreement)

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

PVS SBCL Binaries

PVS CMU Lisp Binaries

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.

PVS Sources

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:

See the included INSTALL file for build instructions.

PVS Binaries Installation

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 Notes

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.


Earlier Versions


Downloading PVS 3.2

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


Downloading PVS 3.1

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.


Downloading PVS 3.0

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.


Downloading PVS 2.4

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.


Mirror Sites

The files may also be obtained from any of the following mirror sites:

These are automatically updated, but there may be a lag time.


Installing PVS

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.


Installing Even Earlier Versions

Even earlier versions of PVS are still available, though they may have problems on newer platforms.


Installing Everything Else

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.

Home Intro Wiki Docs FAQ Download Bugs Mail FM Tools

Last modified: Wed 30 Jan 2013 02:27 PST
Maintainer: Sam Owre