Analysis of Computer Systems Group

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:

or

(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

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:

In bash use something like the following:

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)

• Binary archives for SunOs, Linux, and Windows.
• The source files.
• The rule files
• The TLV Manual (PS, PDF).

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)

• Compressed TLV executables for Sun, GNU/Linux, or Cygwin (use the command "uncompress" to uncompress these files).
• The source files.
• The rule files (tarred and compressed).
• The TLV manual.
• A TLV tutorial which was used for teaching undergraduate courses on verification.

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.