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
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.
Type de document :
Communication dans un congrès
Dimitra Giannakopoulou and Dominique Méry. 18th International Symposium On Formal Methods - FM 2012, Aug 2012, Paris, France. Springer, 7436, pp.147-154, 2012, Lecture Notes in Computer Science; FM 2012: Formal Methods 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings. <10.1007/978-3-642-32759-9_14>
Liste complète des métadonnées

https://hal.inria.fr/hal-00726631
Contributeur : Stephan Merz <>
Soumis le : mercredi 27 mars 2013 - 10:09:08
Dernière modification le : jeudi 9 février 2017 - 15:43:40

Fichier

final.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, et al.. TLA+ Proofs. Dimitra Giannakopoulou and Dominique Méry. 18th International Symposium On Formal Methods - FM 2012, Aug 2012, Paris, France. Springer, 7436, pp.147-154, 2012, Lecture Notes in Computer Science; FM 2012: Formal Methods 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings. <10.1007/978-3-642-32759-9_14>. <hal-00726631>

Partager

Métriques

Consultations de
la notice

370

Téléchargements du document

286