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.
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
% 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.
An updated tutorial is not yet available.
Note for Windows users:
Download previous stable version (3.2)
Note: this version is unsupported and, to be honest, rather old.
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)