TLA+ Proofs - Archive ouverte HAL Access content directly
Conference Papers Year : 2012

TLA+ Proofs

(1, 2) , (3, 4) , (4, 5) , (4, 6, 7) , (8) , (4, 6, 7)
1
2
3
4
5
6
7
8

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.
Fichier principal
Vignette du fichier
final.pdf (285.16 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-00726631 , version 1 (27-03-2013)

Identifiers

Cite

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⟩
498 View
533 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More