Analysis of Computer Systems Group

Department of Computer Science, New York University


Overview

Installation

Running TLPVS


Download

Links

TLPVS

TLPVS is PVS implementation of a linear temporal logic verification system. The system includes a set of theories defining a temporal logic, a number of proof rules for proving soundness and response properties, and strategies which aid in conducting the proofs. In addition to an implementation of a framework for existing rules, it also has new methods which are particularly useful in a deductive LTL system. A distributed rank rule for the verification of response properties in parameterized systems is presented, and a methodology is detailed for reducing compassion requirements to justice requirements (strong fairness to weak fairness). Special attention has been paid to the verification of unbounded systems - systems in which the number of processes is unbounded - and our - verification rules are appropriate to such systems.

TLPVS was implemented by Tamarah Arons.

Installation

PVS and TLPVS are already installed on eeyore. 
To start PVS simply type ./pvs from any directory. 
In order to run TLPVS follow the instructions in the next section ‘Running TLPVS’.  On eeyore the TLPVS library can be found at /users/ariel/TLPVS.
 
If you want to install TLPVS on your own machine you should do the following:
Requirements:
   PVS installed. Latest version and instructions are available here.
 
Download:
  Download the most recent version of TLPVS into a new directory, e.g. TLPVS
 
Install:
   Run PVS in the TLPVS directory and enter the following commands:
   M-x undump-pvs-files
         Undump the file dump27p12p06.dat into the current working directory.
         undumpting should also create a subdirectory PVSHOME.
   M-x find-pvs-file
         Load the main file temporal_logic_prelude.
   M-x prove-importchain
         Prove all theories imported by the loaded file.
   M-x exit-pvs
         Exit PVS (will create binaries and the .pvscontext file).
 
  (Note that proving all theories may take a couple of minutes.)
 

Running TLPVS

   Place the file pvs-strategies in the working directory. 
 
   Start PVS (by typing ./pvs)
 
   Load the TLPVS library: 
      M-x load-prelude-library
      (The command will ask you for the directory of the library, which is wherever you have installed TLPVS.)
   
   Load your own theory files (e.g. bakery.pvs).

Download

Further Links

The Analysis of Computer Systems web site
PVS
Verifying Transactional Memories with TLPVS
  

LAST UPDATED: 6/10/2008
Maintained by Ariel Cohen (arielc at cs.nyu.edu)