What is TLA+?

TLA⁺ is a formal language for specifying systems that is used in industry and academia to verify complex distributed and concurrent systems. Among others, the TLA⁺ methodology is successfully applied at Amazon Web Services and Microsoft.

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 tools include the TLC model checker, the PlusCal algorithm language and its translator, and the TLA⁺ Proof System.

TLA+ Conference?

The objective of the TLA⁺ Conference is to bring together industrial users of the TLA⁺ specification language and its associated tools; it complements the biannual TLA+ workshops. The conference will consist of invited talks that present 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 but not limited to:

• Industrial and academic case studies
• Use of the TLA⁺ tools or reports on their shortcomings
• Teaching of TLA⁺ in industry or academia
• Novel techniques exploiting TLA⁺ and its tools

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

When?

Proposals for presentations, with a one-page summary of the content, should be sent by July 01, 2019 to <<tla2019» \o <<@» \o <<tlapl.us». Notification of acceptance will be given by July 15, 2019. The abstracts and presentations given at the event will be made available on the web.

Where?

The conference will take place in St. Louis, MO, USA, on September 12, 2019 as part of Strange Loop 2019. Participants are required to register through the Strange Loop web site.

Who?

Organizers: Leslie Lamport, Markus Kuppe