Analysis of Computer Systems Group

Department of Computer Science, New York University


Overview

Installation

Download

Mailing List

Links

TLV — Temporal Logic Verifier

TLV is based on the SMV model checker , however, all the code implementing model checking has been replaced by a layer that implements a scripting language called TLV-Basic. Users of the system can then write procedures in TLV-Basic for implementing either model checking or deductive verification rules. TLV is a byproduct of Elad Shahar's M.Sc. thesis.

Installation

Compressed executables are available for Sun/Solaris, Linux, and win32. To use them, save the file to your disk. Use the following command to uncompress the file:

% tar xvzf  tlv-linux-4.XX.tgz

or


% unzip tlv-win32-4.XX.zip

(Make sure you get the filename right)

You can use the source files to compile TLV on other systems. However, we have only checked Solaris, Linux, Windows XP (MinGW and Cygwin), and Mac OS X. It is easier to compile if you have flex, bison, gcc, and gnu readline. To use the source files, create a new directory, put the file in that directory. Then type

% tar xvzf tlv-rules-4.XX.tgz

If you want to put the rule files in a separate directory, you have to tell TLV where the rule files are. To do this set the environment variable TLV_PATH to point to the directory where the rule files are. For example, in cshell I use the command:

% setenv TLV_PATH /home/elad/tlvd/Modules

In bash use something like the following:
% export TLV_PATH=/home/elad/tlvd/Modules

Currently the compiler from SPL to SMV is not available, thus you cannot use tlv to load programs written in SPL.

Download most recent version (4.18.4)

An updated tutorial is not yet available.

Note for Windows users:  For better command line facilities (e.g. command line history), you might want to install Cygwin with development packages, then recompile the sources yourself. The Windows binary distributed here, while not requiring Cygwin, is not so friendly on the command line.

Download previous stable version (3.2)

Note: this version is unsupported and, to be honest, rather old.

Mailing List

A mailing list is available for discussion by both users and (potential) developers. To subscribe, go here.

Further Links

The Analysis of Computer Systems web site

An SMV Mode interface for Emacs. See the file itself for instructions how to set it up.


LAST UPDATED: 10/29/2006
Maintained by Ittai Balaban (balaban at cs `.' nyu `.' edu)