TLA+ Proofs

Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernén Vanzetto

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.

© Springer-Verlag 2012

Available as: PDF

Also available: extended version, TLA+ module

Reference

@InProceedings{cousineau:tla-proofs,
  author =       {Denis Cousineau and Damien Doligez and Leslie Lamport and Stephan Merz and Daniel Ricketts and Hern{\'a}n Vanzetto},
  title =        {TLA\textsuperscript{+} Proofs},
  booktitle = {18th Intl. Symp. Formal Methods (FM 2012)},
  pages =     {147-154},
  year =      2012,
  editor =    {Dimitra Giannakopoulou and Dominique M{\'e}ry},
  volume =    {7436},
  series =    {LNCS},
  address =   {Paris, France},
  publisher = {Springer},
}