TLA+ Proofs
classification
💻 cs.SE
cs.LO
keywords
proofsdescribetlapsalgorithmcheckcomplexconstructsexample
read the original 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 to describe the features of TLAPS and show how it and the Toolbox (an IDE for TLA+) help users to manage large, complex proofs.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.