Important dates

submission: May 20
notification: June 17
final version: July 8
workshop: August 27


TLA+ is a formal language for specifying systems that is seeing some use in industry. TLA+ tools include the TLC model checker, the PlusCal algorithm language and translator, and the TLA+ Proof System. The TLA+ Toolbox is an Integrated Development Environment for writing TLA+ specifications and running the tools on them.

The TLA+ workshop is a forum for practitioners and researchers interested in the use and further development of the TLA+ specification language and its associated tools. Presentations of academic or industrial use of TLA+ or PlusCal, of extensions to the existing tools or of the innovative use of these tools are of particular interest.

The workshop will take place in Paris, France, as a satellite of FM 2012. Participants are required to register through the FM 2012 Web site. There will be no formal workshop proceedings; accepted papers and presentations will be posted on the Web site of the workshop and will be made available to attendees of FM 2012.