Holzmann, Gerard J. (2015) Tau -- a lightweight tool for specifying and verifying tiny automata models. [Software] (Unpublished) https://resolver.caltech.edu/CaltechAUTHORS:20191028-150942118
![]() |
Archive (GZIP) (tau tool)
- Submitted Version
Creative Commons GNU LGPL (Software). 20kB |
Use this Persistent URL to link to this item: https://resolver.caltech.edu/CaltechAUTHORS:20191028-150942118
Abstract
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: |
| ||||||
Subject Keywords: | formal verification, finite automata, omega automata, linear temporal logic, LTL, logic model checking | ||||||
Record Number: | CaltechAUTHORS:20191028-150942118 | ||||||
Persistent URL: | https://resolver.caltech.edu/CaltechAUTHORS:20191028-150942118 | ||||||
Usage Policy: | No commercial reproduction, distribution, display or performance rights in this work are provided. | ||||||
ID Code: | 99504 | ||||||
Collection: | CaltechAUTHORS | ||||||
Deposited By: | Katherine Johnson | ||||||
Deposited On: | 28 Oct 2019 22:14 | ||||||
Last Modified: | 28 Oct 2019 22:14 |
Repository Staff Only: item control page