DrTLAPlus

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.