/DrTLAPlus

Dr. TLA+ series - learn an algorithm and protocol, study a specification

Primary LanguageTLA

Dr. TLA+ Series - learn an algorithm and protocol, study a specification

Lecture schedule (Time: 10-11:30am PDT)

Date Speaker Topic Media
06.22.2016 Andrew Helwer Paxos video, slides
07.21.2016 Jin Li Raft video, slides
08.29.2016 Cheng Huang Fast Paxos video, slides
09.23.2016 Rustan Leino Global Snapshots video, slides
11.09.2016 Heidi Howard Flexible Paxos video, slides
01.20.2017 Shuai Mu Byzantine Paxos video, slides
03.01.2018 Ed Huang Verifying Distributed Transaction with TLA+ in TiDB
11.01.2018 Murat Demirbas Consistency guarantees provided by Cosmos DB video, slides
11.15.2019 Saksham Chand Specification and Verification of Multi-Paxos video, slides
02.XX.2021 Stephan Merz & Markus Kuppe Termination Detection (EWD840 & EWD998)

Each session will focus on a single algorithm/protocol and:

  • dive deep into how the algorithm and protocol works;
  • illustrate in detail how the TLA+ specification is written;
  • share the learnings from writing and studying the specification.