A Caltech Library Service

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

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

[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:20191028-150942118
Persistent URL:
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:99504
Deposited By: Katherine Johnson
Deposited On:28 Oct 2019 22:14
Last Modified:28 Oct 2019 22:14

Repository Staff Only: item control page