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. 〈10.1007/978-3-642-32759-9_14〉
Liste complète des métadonnées

Littérature citée [14 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00726631
Contributeur : Stephan Merz <>
Soumis le : mercredi 27 mars 2013 - 10:09:08
Dernière modification le : mercredi 8 novembre 2017 - 12:08:08
Document(s) archivé(s) le : vendredi 31 mars 2017 - 12:08:16

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. 〈10.1007/978-3-642-32759-9_14〉. 〈hal-00726631〉

Partager

Métriques

Consultations de la notice

445

Téléchargements de fichiers

353