A Caltech Library Service

Tau -- a lightweight tool for specifying and verifying tiny automata models

Holzmann, Gerard Tau -- a lightweight tool for specifying and verifying tiny automata models. [Software] (Unpublished)

WarningThere is a more recent version of this item available.

[img] Archive (GZIP) (tau tool) - Submitted Version
Creative Commons GNU LGPL (Software).


Use this Persistent URL to link to this item:


Tau is a small Tcl/Tk application that can be used to quickly specify and formally verify small automata models (the name 'tau' is short for 'tiny automata') It is used as a teaching aid in CS118, a course on the formal verification of asynchronous software systems using logic model checking. Tau requires the availability of a standard C compiler (e.g., gcc) and a recent version of the Spin model checker (e.g., Version 6.4.3 or later) as background tools.

Item Type:Software
Related URLs:
URLURL TypeDescription ItemSpin model checker (used as a background verification engine)
Contact Email
Subject Keywords:formal verification, finite automata, omega automata, linear temporal logic, LTL, logic model checking,
Record Number:CaltechAUTHORS:20150211-111542706
Persistent URL:
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:54720
Deposited By: Gerard Holzmann
Deposited On:11 Feb 2015 21:01
Last Modified:03 Oct 2019 08:00

Available Versions of this Item

Repository Staff Only: item control page