Analysis of Computer Systems Group

Department of Computer Science, New York University

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

The dump of Tlpvs Prelude for PVS 4.0 (12/27/2006 by Yaniv Sa'ar)
The old dump file (4/18/2004 by Tamarah Arons)
pvs-strategies
TLPVS’s old user-guide
TLPVS: A pvs-Based LTL Verification system - A link to a paper by Amir and Tamarah giving an overview of TLPVS.

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)