Download: PDF.
“Reasoning about TLA Actions” by Carlos Pacheco. May 2001. Undergraduate honors thesis.
We use the ACL2 theorem prover to verify invariants of a distributed algorithm specified in TLA (Temporal Logic of Actions). The algorithm, Disk Synod, achieves consensus among a set of processors communicating through disks. We discuss the translation of TLA specifications into a finite set theory framework in ACL2, as well as the proof of two invariant properties of Disk Synod.
Download: PDF.
BibTeX entry:
@misc{PachecoTh2001, author = {Carlos Pacheco}, title = {Reasoning about TLA Actions}, number = {TR01-16}, month = may, year = {2001}, note = {Undergraduate honors thesis}, organization = {The University of Texas at Austin} }