Skip to content

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

Notifications You must be signed in to change notification settings

tlaplus/DrTLAPlus

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

71 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

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

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.