swMATH ID: 4442
Software Authors: L. Lamport
Description: TLA stands for the Temporal Logic of Actions, but it has become a shorthand for referring to the TLA+ specification language and the PlusCal algorithm language, together with their associated tools. TLA+ is based on the idea that the best way to describe things formally is with simple mathematics, and that a specification language should contain as little as possible beyond what is needed to write simple mathematics precisely. TLA+ is especially well suited for writing high-level specifications of concurrent and distributed systems. PlusCal is an algorithm language that, at first glance, looks like a typical tiny toy programming language. However, a PlusCal expression can be any TLA+ expression, which means anything that can be expressed with mathematics. This makes PlusCal much more expressive than any (real or toy) programming language. A PlusCal algorithm is translated into a TLA+ specification, to which the TLA+ tools can be applied. The principal TLA+ tools are the TLC model checker and TLAPS, the TLA+ proof system. All the tools are normally used from the Toolbox, an IDE (integrated development environment). Go to the TLA home page to find out more about TLA.
Homepage: http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html
Related Software: SPIN; z3; Z; ByMC; Uppaal; PEPA; Isabelle/UTP; Verdi; Distal; PSync; nuXmv; MathSAT5; SPLLIFT; Featherweight Java; PlusCal; LaTeX; TLAPS; Mizar; Design/CPN; Intel TBB
Referenced in: 26 Publications
Further Publications: http://research.microsoft.com/en-us/um/people/lamport/tla/papers.html

Referencing Publications by Year