Tampere Verification Tool



23 Mar, 2012

4 Oct, 2006

24 May, 2005:

22 March, 2004:

20 May, 2003:

21 February, 2003:

Previous news.

What is TVT?

TVT --Tampere Verification Tool-- is a toolset for error detection and automatic verification of concurrent and reactive systems. One of the key features of TVT is the support for both action and state based verification. This is made possible by the labelled state transition system (LSTS), the formal model used in TVT. LSTS is used to represent either the behaviour of a complete system or the behaviour of a component of a system.

TVT provides tools for advanced state space methods, and a framework for further tool development. It is published under the NOKOS open source license to welcome third parties in future development. The current version 3.0.1 has been built in the years 1999-2004.

For more information about theoretical concepts, see VARG homepage.

For information about the license agreement, see http://www.opensource.org/licenses/nokia.html.

Who are involved?

TVT was originally built for Nokia Research Centre and the development work was mainly done at Tampere University of Technology (TUT for short) Institute of Software Systems and within the institute by the Verification Algorithm Research Group. The work continues for now at TUT.

More info on TVT

The presentation slides of TVT Release day, November 12. 2001, Helsinki:

Related work

We encourage others to join in the development of TVT and any tools and other additions to it.

TVT online documentation for the version 3.0

Downloads and examples

TVT is published under the NOKOS license. Please read the license before downloading.

Henri Hansen, hansen@cs.tut.fi.
Timo Erkkilä, timo{dot}erkkila{at}tut{dot}fi.
Last modifications to this page: Tue Oct 24 14:50:26 EET 2006 by Antti Kervinen