Verifying TLA+ Invariants with ACL2

Download: PDF.

“Verifying TLA+ Invariants with ACL2” by Carlos Pacheco. Aug. 2001. Research report for the Educational Advancement Foundation, August 2001. An abridged version appeared in Selected 2001 SRC Summer Intern Reports, Technical Note 2001-004, Compaq Systems Research Center, December 2001.

Abstract

We describe the use of the ACL2 theorem prover to model and verify properties of TLA+ specifications. We have written a translator whose input is a TLA+ specification along with conjectures and structured proofs of properties of the specification. The translator's output is an ACL2 model of the specification, and a list of ACL2 conjectures corresponding to those sections of the proof outlines flagged for mechanical verification. We have used our tools to translate the Disk Synod algorithm, and to verify two invariants of the algorithm.

Download: PDF.

BibTeX entry:

@misc{PachecoSRC2001,
   author = {Carlos Pacheco},
   title = {Verifying TLA+ Invariants with ACL2},
   month = aug,
   year = {2001},
   note = {Research report for the Educational Advancement Foundation,
	August 2001. An abridged version appeared in Selected 2001 SRC
	Summer Intern Reports, Technical Note 2001-004, Compaq Systems
	Research Center, December 2001}
}