PVS releases are available with Allegro Common Lisp or SBCL. Current versions are for Linux and MacOSX 64-bit machines. If you have other platforms, you may be able to use Vagrant with a Linux version, use an earlier release, or contact us at firstname.lastname@example.org to discuss possibilities.
Vagrant: any operating system that supports Vagrant and Virtualbox (e.g., Windows) should be able to run PVS 7.1 or later. Simply download a Linux version of PVS, untar it, and follow the instructions in vagrant.README.
We strongly suggest getting a pre-built Allegro version, unless you have concerns with the Allegro runtime click-though license, in which case get one of the SBCL Lisp images. It is also possible to build PVS from GitHub sources, but it can be sensitive to the platform environment. If you decide to try it and run into problems, please let us know at email@example.com.
In PVS Version 7 and later, simply untar the file where you want, and a subdirectory will be created for you. For earlier versions you should create a subdirectory, cd to it, and untar from there.
Then read the INSTALL file to finish installation.
In general, the Allegro version is faster, but does require agreeing to a click-through license for Allegro, also included in the tar file as LICENSE-SRI. The PVS sources are under GPL.