TLA+ Proofs
Software Engineering
2012-08-30 v1 Logic in Computer Science
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.
Cite
@article{arxiv.1208.5933,
title = {TLA+ Proofs},
author = {Denis Cousineau and Damien Doligez and Leslie Lamport and Stephan Merz and Daniel Ricketts and Hernán Vanzetto},
journal= {arXiv preprint arXiv:1208.5933},
year = {2012}
}
Comments
A shorter version of this article appeared in the proceedings of the conference Formal Methods 2012 (FM 2012, Paris, France, Springer LNCS 7436, pp. 147-154)