TLA+ Community Event 2025

Co-located with ETAPS 2025 in Hamilton, Ontario (Canada), on May 4, 2025.

TLA+ is a language that is used in academia and industry for formally specifying systems. It is supported by verification tools, including the TLC and Apalache model checkers and the TLAPS proof system. PlusCal serves as a frontend for generating TLA+ specifications from an algorithmic language with an imperative flavor.

The TLA+ Community Event serves as a forum where practitioners and researchers interested in the use and further development of the TLA+ specification language and its tools meet and discuss.

Proposals for contributed talks are sollicited that present work of interest to users of TLA+ or PlusCal, such as:

• industrial or academic case studies,
• new tools for TLA+ or add-ons to existing tools,
• innovative use of existing tools or reports on their shortcomings,
• use of TLA+ in education.

Proposals for presentations, with a short (2 page) abstract summarizing the content, should be sent to tla2025@inria.fr by February 7, 2025. Please indicate if you want to give a short or long presentation (25 or 40 minutes, including discussion). Notification will be given by February 17, 2025.

There will not be formal proceedings, but the abstracts and presentations will be made available on the Web.

Participants will be required to register to ETAPS 2025.

Organizers

• Igor Konnov, researcher in security and formal methods and TU Wien
• Markus Kuppe, Microsoft
• Stephan Merz, Inria Nancy

Program committee

TBA