| 09:00 | Keynote: TLA+ in Engineering Systems: Quinceañera | David Langworthy | pptx | video |
| 10:00 | Modeling Virtual Machines and Interrupts in TLA+ and PlusCal | Valentin Schneider | pdf | video |
| 10:30 | Coffee break | | | |
| 11:00 | An Animation Module for TLA+ | William Schultz | pdf | video |
| 11:45 | BMCMT: Bounded Model Checking of TLA+ Specifications with SMT | Igor Konnov, Jure Kukovec, Thanh Hai Tran | pdf | video |
| 12:30 | Lunch | | | |
| 14:00 | Applying TLA+ in a Safety-Critical Railway Project | Stefan Resch | pdf | video |
| 14:30 | Tutorial: State Space Explosion or: How To Fight An Uphill Battle | Markus Kuppe | pdf | video |
| 15:30 | Coffee Break | | | |
| 16:00 | Proving Properties of a Minimal Covering Algorithm | Ioannis Filippidis, Richard M. Murray | pdf | |
| 16:45 | Invariants in Distributed Algorithms | Annie Liu, Scott D. Stoller, Saksham Chand, Xuetian Weng | pdf | video |
| 17:30 | Discussion and wrap-up | | | |
| 18:00 | End of the meeting | | | |