TLA+ Community Event 2025
Sunday, May 4, 2025
Hamilton, Canada
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:
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.
| time | title | speaker | affiliation | slides | recording |
|---|---|---|---|---|---|
| 08:55 | Welcome & Opening Announcements | ||||
| 09:00 | Formal models for monotonic pipeline architectures | J.-P. Bodeveix, A. Bonenfant, T. Carle, M. Filali, C. Rochange | |||
| 09:45 | ModelFuzz: Model guided fuzzing of distributed systems | Srinidhi Nagendra | Max Planck Institute for Software Systems | ||
| 10:30 | Coffee Break | ||||
| 10:45 | Translating C to PlusCal for Model Checking of Safety Properties on Source Code | Guillaume DI FATTA, Emmanuel Ohayon, and Amira Methni | Asterios Technologies | ||
| 11:30 | TLA+ for All: Model Checking in a Python Notebook | Konstantin Läufer & George K. Thiruvathukal | Loyola University Chicago | ||
| 12:00 | Lunch | ||||
| 13:00 | TLA+ Modeling of MongoDB Transactions | Murat Demirbas & Will Schultz | MongoDB | ||
| 13:45 | Automating Trace Validation with PGo | Finn Hackett & Ivan Beschastnikh | University of British Columbia | ||
| 14:30 | Coffee Break | ||||
| 14:45 | It’s never been easier to write TLA⁺ tooling! | Andrew Helwer | txt | ||
| 15:15 | Are We Serious About Using TLA+ For Statistical Properties? | A. Jesse Jiryu Davis | MongoDB | txt | |
| 15:45 | Discussion Panel | ||||
| 16:00 | Closing Remarks | ||||
| 16:15 | End of the conference |