TLA+ Community Event 2020
October 15.-16. & 19.
Virtual

TLA+ Community Event 2020

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
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