The virtual hallway and channels to ask the speakers questions can still be found at
http://talk.tlapl.us.
| time (CEST) | title | speaker | slide | recording |
|---|
| Thursday, October 15 | | | |
| 5:30pm | Welcome | | | |
| 5:40pm | Keynote: TLA+ at Microsoft to build planetary-scale systems | Dharma Shukla | ppt | video |
| | | | |
| Friday, October 16 | | | |
| 3:00pm | Conjunction Capers (TLA+ Truffle) | Ron Pressler | pdf | video |
| 3:25pm | Bridging the Verifiability Gap: Why We Need More From Our Specs and How We Can Get It | Jordan Halterman | pdf | video |
| 3:50pm | break | | | |
| 4:15pm | A formal model of cache speculation side channels | Catalin Marinas | pdf | video |
| 4:40pm | Exploring and improving the design of Abaco | Smruti Padhy, Joe Stubbs | pdf | video |
| 5:05pm | break | | | |
| 5:30pm | eXtreme Modelling in Practice (paper) | Jesse Davis, Max Hirschhorn, Judah Schvimer | | video |
| 5:55pm | Kayfabe – model-based program testing | Star Dorminey | ppt | video |
| 6:20pm | Model-based testing with TLA+ and Apalache | Andrey Kupriyanov, Igor Konnov | pdf | video |
| | | | |
| Monday, October 19 | | | |
| 3:00pm | Checking safety in Exactly-once - a library for stronger message processing guarantees | Tomek Masternak, Szymon Pobiega | pdf | video |
| 3:25pm | TLA + specification of PCR parallel programming pattern | Jose Solsona, Sergio Yovine | pdf | video |
| 3:50pm | break | | | |
| 4:15pm | TLA+ validation of Chord | Jean-Paul Bodeveix, Julien Brunel, David Chemouil, Mamoun Filali | pdf | video |
| 4:40pm | An Extension of PlusCal for Modeling Distributed Algorithms | Heba Alkayed, Horatiu Cirstea, Stephan Merz | pdf | video |
| 5:05pm | break | | | |
| 5:30pm | Higher-order Automation in TLAPS | Antoine Defourné, Petar Vukmirovic | | video |
| 5:55pm | Type Inference for TLA+ in Apalache | Jure Kukovec, Igor Konnov | | video |
| 6:20pm | Discussion and wrap-up | | | |
v1.0