TLA+ Proofs

Denis Cousineau 1 Damien Doligez 2, 3 Leslie Lamport 3, 4 Stephan Merz 3, 5, 6 Daniel Ricketts 7 Hernán Vanzetto 3, 5, 6
5 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
6 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
7 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 TLA+ 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. A shorter version of this article was published at the conference Formal Methods 2012.
Type de document :
Communication dans un congrès
AI meets Formal Software Development, Jul 2012, Dagstuhl, Germany. 16 p., 2012, 〈http://arxiv.org/abs/1208.5933〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00726632
Contributeur : Stephan Merz <>
Soumis le : jeudi 30 août 2012 - 19:42:28
Dernière modification le : mercredi 20 février 2019 - 01:08:17

Identifiants

  • HAL Id : hal-00726632, version 1

Citation

Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, et al.. TLA+ Proofs. AI meets Formal Software Development, Jul 2012, Dagstuhl, Germany. 16 p., 2012, 〈http://arxiv.org/abs/1208.5933〉. 〈hal-00726632〉

Partager

Métriques

Consultations de la notice

434