A Caltech Library Service

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

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

This is the latest version of this item.

[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)
Subject Keywords:formal verification, finite automata, omega automata, linear temporal logic, LTL, logic model checking
Record Number:CaltechAUTHORS:20150324-144547664
Persistent URL:
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:56038
Deposited By: Gerard Holzmann
Deposited On:24 Mar 2015 23:03
Last Modified:03 Oct 2019 08:10

Available Versions of this Item

Repository Staff Only: item control page