Skip to Main content Skip to Navigation
Conference papers

TLA+ Proofs

Denis Cousineau 1, 2 Damien Doligez 3, 4 Leslie Lamport 4, 5 Stephan Merz 4, 6, 7 Daniel Ricketts 8 Hernán Vanzetto 4, 6, 7
2 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
6 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
7 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
8 Department of Computer Science
CSE-UCSD - Department of Computer Science and Engineering [San Diego]
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 \tlaplus 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [14 references]  Display  Hide  Download
Contributor : Stephan Merz Connect in order to contact the contributor
Submitted on : Wednesday, March 27, 2013 - 10:09:08 AM
Last modification on : Tuesday, January 11, 2022 - 11:16:26 AM
Long-term archiving on: : Friday, March 31, 2017 - 12:08:16 PM


Files produced by the author(s)



Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, et al.. TLA+ Proofs. 18th International Symposium On Formal Methods - FM 2012, Aug 2012, Paris, France. pp.147-154, ⟨10.1007/978-3-642-32759-9_14⟩. ⟨hal-00726631⟩



Les métriques sont temporairement indisponibles