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
The theory was implemented in PVS
The implementation is available as
a gzip'd tarball.
To replay the whole proof, follow the instructions below.
Download and install
PVS version 3.2.
(Higher versions seem not work.)
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:
- Extract the theory implementation and
move the file named .pvs.lisp to your home directory.
This fixes some PVS bugs.
- Change to the directory where *.pvs and *.prf files are extracted
and type pvs. PVS will start up with an Emacs frontend.
- Type C-c C-f to load the example.pvs
into an Emacs buffer.
- 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.
- 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.
Back to Susumu Nishimura's homepage.