The Program Verification System (PVS) is a formal verification system developed by SRI International. PVS provides a rich specification language based on a strongly-typed higher-order logic and a powerful theorem prover for this logic. The PVS type system supports sub-typing and dependent types. The theorem prover includes decision procedures and simplification strategies for a variety of theories.
PVS is a key component of several formal verification projects at NASA Langley. For that reason, NASA Langley supports a PVS Research effort that aims at the advancement of theorem proving techniques for complex safety-critical applications. The Formal Methods group at NASA Langley, in collaboration with the PVS community, develops and maintains the PVS NASA Libraries, a large collection of PVS developments that range from fundamental mathematical theories to frameworks for the verification of air traffic systems and fault-tolerant protocols.
PVS runs on Linux, Solaris, and Mac OS X. Participants of the PVS
Class 2012 are expected
to have the latest version of PVS,
(Allegro binaries are suggested),
and the latest version of the NASA PVS Libraries, currently 5.8,
installed in their laptops. Please, follow the provided
to install these libraries in your system.
Ask the organizers if you have
problems installing PVS or the NASA Libraries. The PVS Class 2012 lectures, exercises, and solutions are
electronically available as compress files (
ISO image file (370Mb) of a CD containing all the material prepared
for this class is also avialable.
Browse the content of the CD through the file
There is not a native Windows version of PVS. However, PVS can be installed in a virtual Linux machine, which can be executed in a Windows platform using a virtualizer tool such a VirtualBox, VMWare, etc. As a convenience to attendants bringing Windows laptops, we have prepared a virtual Ubuntu 12.04 machine, for VirtualBox. See instructions below for downloading and installing the pre-configured virtual machine. The virtual machine already includes everything that is needed for the PVS Class 2012 (you don't need to download these files, they are alreay included in the virtual machine hard drive):
The pre-condigured virtual machine is largely platform-independent and can be used under any host supported by Virtual Box, e.g., Windows, Linux, and Mac OS X.
To create the pre-configured virtual machine in your laptop (host), you need to download these files:
Once you have installed VirtualBox and, optionally, the Extension
Pack, and uncompressed the file
NASA-NIA_PVS_Class_2012_SBCL.vdi.gz), follow these steps to
create a virtual machine in VirtualBox:
New, give a name to the machine, e.g.,
PVSClass2012, its type is
Linux, and its version
Use an existing virtual hard drive fileand click on the small folder icon to open a file browser.
NASA-NIA_PVS_Class_2012.vdiin the file browser and click
We recommend that you create a directory in your laptop to be shared with your virtual machine. A shared directory is a convenient way to transfer files between your laptop and the virtual machine. To configure a shared directory between the laptop and the virtual machine, follow these steps:
Settings(make sure that the machine that is selected is the one you just created).
Folder Path, select the directory in your laptop to be shared with the virtual machine.
Auto-mountand, if there is one, the box
Now, you are ready to execute the virtual machine. Go again to the
VirtualBox window, make sure that the machine that is selected is the
one you just created, and click
Start. If everything
goes well you will have our pre-configured Ubuntu machine up and
running in your laptop. The default user of the machine is
and its password is also
In the virtual machine, you can launch PVS 5.0 directly from the side bar of the Ubuntu
interface. Just click on the PVS
icon. PVS 5.0 is installed in the directory
and the default context directory is
PVS-5.0/pvsclass2012/exercises. We have copied all
the exercises into this directory. Hence, once you launch PVS by using
the icon in the side bar you are ready to
start working on the PVS Class
2012. Solutions to the exercises are available in
PVS-5.0/pvsclass2012/solutions, but don't look at them yet.
In the desktop of your Ubuntu virtual machine, there are three shortcuts:
Shared Host Boxpoints to the shared directory
/media/sharedboxbetween the laptop and the virtual machine.
PVS-5.0 Documentspoints to the directory
PVS-5.0/docthat contains PVS manuals.
PVS Class 2012points to the program and lectures of the PVS Class 2012.
If you want to be able to access from your virtual machine a USB memory pen plugged to your laptop, you have to install VirtualBox 4.2 Oracle VM VirtualBox Extension Pack in your laptop. Once this package is installed, follow these steps:
Portsand then on
Enable USB 2.0 (EHCI) Controller.
USB Device Filterslist area to create a filter with default values.
Both Mac OS X and Windows have standard tools for
zip files. However,
those tools don't handle very well large files, such as the
virtual hard drives provided here. The uncompressed file is 4.7 G. The
message in Windows 7 about needing additional 734TB is, of course, an error. It has been reported that the
following tools correctly uncompress those files:
Files with extension
gz can be uncompressed with
gunzip, which is standard in Linux and Mac OS X. For
Windows, see the Gzip web site.