PVS   Based Proofs Of Safety Properties of Access Graphs Operations

Parvati Chandrasekhar Iyer,
(parvati.iyer[AT]gmail.com)
Indian Institute of Information Technology,Allahabad


This directory contains the specification and proofs of the safety properties of access graphs which have been defined in

Uday Khedker, Amitabha Sanyal, Amey Karkare. Heap Reference Analysis Using Access Graphs, Department of Computer Science & Engg., IIT Bombay. 2005 (In Preparation). (Abstract)

These specifications and proofs were developed using the PVS Prototype and Verification System. This work was done as a part of summer project under IIT BOmbay Summer Internship Scheme and continued later as external B.Tech. project at IIT Bombay.

The following resources have been provided :
  1.  pvs_code.tgz contains 2 files : operations.pvs and the corresponding proof file operations.prf. These are to be used with the PVS system.
  2.  pvs_proof_scripts contains the proof scripts that specify the PVS commands used to develop these proofs. 
  3.  proofs_PS_Documents contains the proofs developed using the PVS system - a knowledge of PVS is not required to interpret these proofs. 
  4.  access_graphs.ps.gz contains the specification based on which the above mentioned proofs were developed - a knowledge of PVS is not required to interpret this specification. 
The resources here have been provided in good faith without any warranty, explicit or implied, towards anything. All copyrights are held by IIT Bombay. For more details, please contact Uday Khedker.