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
1 LRI - Laboratoire de Recherche en Informatique
2 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
3 GALLIUM - Programming languages, types, compilation and proofs
Inria Paris-Rocquencourt
4 MSR - INRIA - Microsoft Research - Inria Joint Centre
5 Microsoft Research [Redmond]
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 metadatas

Cited literature [14 references]  Display  Hide  Download
https://hal.inria.fr/hal-00726631
Contributor : Stephan Merz <>
Submitted on : Wednesday, March 27, 2013 - 10:09:08 AM
Last modification on : Wednesday, August 7, 2019 - 12:18:06 PM
Long-term archiving on : Friday, March 31, 2017 - 12:08:16 PM

File

final.pdf
Files produced by the author(s)

Identifiers

Collections

INRIA | UMR8623 | UNIV-LORRAINE | LORIA-FM | LORIA | INRIA-ROCQ

Citation

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⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

793

Files downloads

529

Contact


archive-ouverte@inria.fr