TLA+ is a formal specification language used to design, model and verify systems

Technologies
java, ocaml, tla+, eclipse, smt
Topics
algorithms, formal methods
TLA+ is a formal specification language used to design, model and verify systems

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.

2018 Program

Successful Projects

Contributor
Parv Mor
Mentor
Markus Kuppe, tla+guru
Organization
TLA+
CONCURRENT ON-THE-FLY SCC-BASED LTL MODEL CHECKING
Project aims at implementation and proof of concurrent on-the-fly SCC detection algorithm to aid in liveness checking of TLC model checker. The goal...