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
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 : vendredi 25 mai 2018 - 12:02:07
Document(s) archivé(s) le : vendredi 31 mars 2017 - 12:08:16

Fichier

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

Identifiants

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. 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〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

738

Téléchargements de fichiers

440

Contact


archive-ouverte@inria.fr