The old (1997-2004) John Von Neumann Minerva Center for
Verification of Reactive Systems



go to the current TLV page at NYU

TLV - Temporal Logic Verifier

TLV is based on the SMV model checker, however, all the code implementing model checking has been thrown out and replaced by a layer which 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.

Spring Term Project 2002

If you are doing the term project for Spring 2002, there is a new update you have to download. One of the rule files has been updated to include the rule well-lex.

So download this deductive.tlv and save it over the old deductive.tlv (alternatively, you can put it in the same directory from which you are testing your algorithms).

Installation

Compressed executables are available for Sun/Solaris, Linux, and cygwin. To use them, save the file to your disk; your browser may uncompress them automatically. However, if the resulting file has a ".Z" suffix then it is still compressed. Use the command "uncompress" to uncompress the file, for example: 

   % uncompress tlvlinux.Z

You can use the source files to compile TLV on other systems, however, we have only checked Solaris, Linux and cygwin. 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 

   % zcat src.tar.Z | tar xvf -
Then, type "make" .

Additionally, you should download a set of rule files which implement verification procedures in TLV-Basic. The rule files also contain a simple example of model checking mutual exclusion using semaphores. For easy installation, open it in the directory in which you intend to work, using the following command: 

   % zcat rules.tar.Z | tar xvf -

If you want to put the rule files in a separate directory, you have to tell TLV where the rule files are. So 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

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.14)

This is Elad's last version.

An updated tutorial is not yet available.

Download previous stable version (3.2)

LAST UPDATED: 29.2.2004
Dept. of Computer Science and Applied Math
The Weizmann Institute of Science
Rehovot 76100, Israel
TelePhone: +972-8-934-3434
Telefax: +972-8-934-4122
To comment on this service, send feedback to the Nir Piterman 		Weizmann Institute