Distributed algorithms in TLA (abstract)
Leslie Lamport · 2000
TLA (the temporal logic of actions) is a simple logic for describing and reasoning about concurrent systems. It provides a uniform way of specifying algorithms and their correctness properties, as well as rules for proving that one specification satisfies another. TLA+ is a formal specification language based on TLA, and TLC is a model checker for TLA+ specifications. TLA+ and TLC have been used to specify and check high-level descriptions of real, complex systems. Because TLA+ provides the full power of ordinary mathematics, it permits simple, straightforward specifications of the kinds of algorithms presented at PODC.