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

TLA+ Proofs

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

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.
Not file

Dates and versions

hal-00726632 , version 1 (30-08-2012)

Identifiers

  • HAL Id : hal-00726632 , version 1

Cite

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. ⟨hal-00726632⟩
365 View
1 Download

Share

Gmail Facebook Twitter LinkedIn More