Holzmann, Gerard J. (2015) Tau -- a lightweight tool for specifying and verifying tiny automata models. [Software] (Unpublished) https://resolver.caltech.edu/CaltechAUTHORS:20191028-150942118
![[img]](https://authors.library.caltech.edu/style/images/fileicons/application_x-gzip.png) |
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
