Important dates

submission: April 25
notification:   April 29
workshop: June 3


TLA+ is a formal language for specifying systems that is used in academia and industry. Tool support for TLA+ is provided through the TLA+ Toolbox, an Integrated Development Environment for writing TLA+ specifications and analyzing them using the TLA+ tools. The main tools include the TLC model checker, the PlusCal algorithm language and translator, and the TLA+ Proof System.

The objective of the TLA+ Community Event is to bring together practitioners and researchers interested in the use and further development of the TLA+ specification language and its associated tools. It will consist of tutorials that present recent developments concerning the TLA+ language and tools, and of contributed talks.

Contributed talks should present work of interest to users of TLA+ or PlusCal, such as:

The presentations should be informal and leave sufficient time for discussions. There will not be formal proceedings, and presentations of relevant work published elsewhere are welcome.

Proposals for presentations, with a short (1-2 page) abstract summarizing the content, should be sent by April 25, 2014 to Notification will be given by April 29, 2014. The abstracts and presentations given at the event will be made available on the Web.

The workshop will take place in Toulouse, France, on June 3, 2014, and will be colocated with ABZ 2014. Participants are required to register through the ABZ 2014 Web site.

Organizers: Leslie Lamport, Stephan Merz, Philippe Quéinnec