The PVS implementation of the MPC'08 paper

This page provides a full implementation of the results of my research paper "Safe Modification of Pointer Programs in Refinement Calculus", to appear in MPC'08 conference. The theory was implemented in PVS theorem prover.

• The implementation is available as a gzip'd tarball.

• To replay the whole proof, follow the instructions below.

  1. Download and install PVS version 3.2. from SRI. (Higher versions seem not work.)

  2. Download NASA Langley PVS libraries for PVS version 3.2 from NASA Langley Research Center and follow the installation note. Most typically you are instructed to:

     • Change directory to the PVS installation directory and type

               tar zxvf the_pvs_library_ver3.2.tgz

       This will extract the libraries under the lib subdirectory.

     • Set the environment variable PVS_LIBRARY_PATH to the lib subdirectory (avoid a trailing /) appropriately, according to the shell you are in use:

       • for csh, tcsh, etc.

                 setenv PVS_LIBRARY_PATH "/pvs/installation/directory/lib"

       • for bash, etc.

                 export PVS_LIBRARY_PATH="/pvs/installation/directory/lib"

  3. Extract the theory implementation and move the file named .pvs.lisp to your home directory. This fixes some PVS bugs.

  4. Change to the directory where *.pvs and *.prf files are extracted and type pvs. PVS will start up with an Emacs frontend.

  5. Type C-c C-f to load the example.pvs into an Emacs buffer.

  6. Type M-x pri in that buffer; simply type return when you are asked for an input in minibuffer. Wait for a while until PVS finishes all the proofs.

  7. When everything is done, "PVS Status" buffer will show up to display the status of all the proofs.

     Here is the status list produced by a run in my own environment.