| HAL-Inria | Publications, software ... of Inria's scientists |
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]
Denis Cousineau 1, 2
Mail :
Author
Damien Doligez 3, 4
Mail :
Author Employer institution : Institut National de Recherche en Informatique et en Automatique IdHAL : damien-doligez
Leslie Lamport 4, 5
Author Employer institution : Microsoft Research
Stephan Merz 4, 6, 7
Mail : Site :
Author IdHAL : stephan-merz ORCID : https://orcid.org/0000-0003-0974-1844
Daniel Ricketts 8
Author Employer institution : University of California [San Diego]
Hernán Vanzetto 4, 6, 7
Author Employer institution : Institut National de Recherche en Informatique et en Automatique
1
LRI - Laboratoire de Recherche en Informatique (LRI - Bâtiments 650-660 Université Paris-Sud 91405 Orsay Cedex - France)
- UP11 - Université Paris-Sud - Paris 11 (Bâtiment 300 - 91405 Orsay cedex - France)
- CentraleSupélec (3, rue Joliot Curie, Plateau de Moulon, 91192 GIF-SUR-YVETTE Cedex - France)
- CNRS - Centre National de la Recherche Scientifique : UMR8623 (France)
2
PROVAL - Proof of Programs (PCRI - Université de Paris-Sud, Bâtiment 650, 91405 ORSAY Cedex - France)
- UP11 - Université Paris-Sud - Paris 11 (Bâtiment 300 - 91405 Orsay cedex - France)
- Inria Saclay - Ile de France (1 rue Honoré d'Estienne d'Orves
Bâtiment Alan Turing
Campus de l'École Polytechnique
91120 Palaiseau - France)
- Inria - Institut National de Recherche en Informatique et en Automatique (Domaine de Voluceau Rocquencourt - BP 105 78153 Le Chesnay Cedex - France)
- CNRS - Centre National de la Recherche Scientifique : UMR (France)
3
GALLIUM - Programming languages, types, compilation and proofs (France)
- Inria Paris-Rocquencourt (INRIA Rocquencourt : Domaine de Voluceau, Rocquencourt B.P. 105 78153 le Chesnay Cedex - France)
- Inria - Institut National de Recherche en Informatique et en Automatique (Domaine de Voluceau Rocquencourt - BP 105 78153 Le Chesnay Cedex - France)
4
MSR - INRIA - Microsoft Research - Inria Joint Centre (Parc Orsay Université 28, rue Jean Rostand 91893 Orsay Cedex FRANCE - France)
- Inria - Institut National de Recherche en Informatique et en Automatique (Domaine de Voluceau Rocquencourt - BP 105 78153 Le Chesnay Cedex - France)
- Microsoft Research Laboratory Cambridge (United Kingdom)
- Microsoft Corporation [Redmond, Wash.] (United States)
5
Microsoft Research [Redmond] (One Microsoft Way, Redmond, WA 98052, USA - United States)
- Microsoft Corporation [Redmond, Wash.] (United States)
6
VERIDIS - Modeling and Verification of Distributed Algorithms and Systems (France)
- MPII - Max-Planck-Institut für Informatik (Campus E-1 4, 66123 Saarbrücken, Germany - Germany)
- Max-Planck-Gesellschaft (Jägerstrasse, 10-11, D-10117 Berlin - Germany)
- Inria Nancy - Grand Est (615 rue du Jardin Botanique 54600 Villers-lès-Nancy - France)
- Inria - Institut National de Recherche en Informatique et en Automatique (Domaine de Voluceau Rocquencourt - BP 105 78153 Le Chesnay Cedex - France)
- LORIA - FM - Department of Formal Methods (France)
- LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications (Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex - France)
- Inria - Institut National de Recherche en Informatique et en Automatique (Domaine de Voluceau Rocquencourt - BP 105 78153 Le Chesnay Cedex - France)
- UL - Université de Lorraine (34 cours Léopold - CS 25233 - 54052 Nancy cedex - France)
- CNRS - Centre National de la Recherche Scientifique : UMR7503 (France)
- LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications (Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex - France)
7
MOSEL - Proof-oriented development of computer-based systems (France)
- LORIA - FM - Department of Formal Methods (France)
- LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications (Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex - France)
- Inria - Institut National de Recherche en Informatique et en Automatique (Domaine de Voluceau Rocquencourt - BP 105 78153 Le Chesnay Cedex - France)
- UL - Université de Lorraine (34 cours Léopold - CS 25233 - 54052 Nancy cedex - France)
- CNRS - Centre National de la Recherche Scientifique : UMR7503 (France)
- LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications (Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex - France)
8
Department of Computer Science (United States)
- CSE-UCSD - Department of Computer Science and Engineering [San Diego] (University of California 9500 Gilman Drive, La Jolla, CA 92093-0404 - United States)
- UC San Diego - University of California [San Diego] (9500 Gilman Dr., La Jolla, CA 92093 USA - United States)
- University of California (United States)
- UC San Diego - University of California [San Diego] (9500 Gilman Dr., La Jolla, CA 92093 USA - United States)
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
https://hal.inria.fr/hal-00726631
Contributor : Stephan Merz <>
Submitted on : Wednesday, March 27, 2013 - 10:09:08 AM
Last modification on : Monday, December 9, 2019 - 5:24:02 PM
Document(s) archivé(s) le : Friday, March 31, 2017 - 12:08:16 PM
Contributor : Stephan Merz <>
Submitted on : Wednesday, March 27, 2013 - 10:09:08 AM
Last modification on : Monday, December 9, 2019 - 5:24:02 PM
Document(s) archivé(s) le : Friday, March 31, 2017 - 12:08:16 PM
File
final.pdf
Files produced by the author(s)
Identifiers
- HAL Id : hal-00726631, version 1
- DOI : 10.1007/978-3-642-32759-9_14
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⟩
Metrics
Record views
818
Files downloads