Skip to Main content Skip to Navigation
Conference papers

TLA+ Proofs

Abstract : TLA+ is a specification language based on standard set theory and temporal logic that has constructs for hierarchical proofs. We describe how to write TLA+ proofs and check them with TLAPS, the TLA+ Proof System. We use Peterson's mutual exclusion algorithm as a simple example and show how TLAPS and the Toolbox (an IDE for TLA+) help users to manage large, complex proofs. A shorter version of this article was published at the conference Formal Methods 2012.
Document type :
Conference papers
Complete list of metadata
Contributor : Stephan Merz Connect in order to contact the contributor
Submitted on : Thursday, August 30, 2012 - 7:42:28 PM
Last modification on : Saturday, October 16, 2021 - 11:26:09 AM


  • HAL Id : hal-00726632, version 1


Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, et al.. TLA+ Proofs. AI meets Formal Software Development, Jul 2012, Dagstuhl, Germany. 16 p. ⟨hal-00726632⟩



Record views