Below is a tentative schedule. Lectures 1-10 and 17 will be taught by me (Gowtham Kaki), while the rest are student-led paper discussions. Lecture slides will be posted after each lecture.

Lecture Date Topic Recommended Reading
1 01/14/2021 Introduction and Logistics Google's Introduction to Distributed Systems Design.
Newcombe et al, Use of Formal Methods at AWS.
Leesatapornwongsa et al, SAMC: Semantic-Aware Model Checking for Fast Discovery of Deep Bugs in Cloud Systems, OSDI'14.
Review of Fundamental Results
2 1/19/2021 Asynchronous Model of a Distributed System
Failure Modes
Time - Ordering of events [Video] 		Lamport, Time, Clocks, and the Ordering of Events in a Distributed System, CACM, 1978
3 1/21/2021 Happens-before, Lamport timestamps, Vector clocks [Video] Lamport, Time, Clocks, and the Ordering of Events in a Distributed System, CACM, 1978
4 1/26/2021 FLP Impossibility [Video] Fischer et al, Impossibility of Distributed Consensus with One Faulty Process, JACM, 1985.
5 1/28/2021 FLP Impossibility (contd.), CAP, PACELC
[Video] 		Lynch et al, Brewer's Conjecture and the Feasibility of Consistent, Available, Partition-Tolerant Web Services, ACM SIGACT News, 2002.
Abadi, Consistency Tradeoffs in Modern Distributed Database System Design: CAP is Only Part of the Story, IEEE Computer, 2012.
Review of Distributed Algorithms
6 2/2/2021 Two-Phase Commit (2PC), Introduction to TLA+ & PlusCal [Video] Lamport, Consensus on Transaction Commit, ACM Transactions on Databases.
Hillel Wayne's TLA+ & PlusCal Tutorials.
7 2/4/2021 2PC in TLA+ & PlusCal [Video] Lamport, Consensus on Transaction Commit, ACM Transactions on Databases.
Marc Brooker's Exploring TLA+ with two-phase commit.
Murat Demirbas's TLA+/Pluscal modeling of 2-phase commit transactions.
8 2/9/2021 Paxos [Video] Lamport, Paxos Made Simple, ACM SIGACT News, 2001.
Chandra et al, Paxos Made Live: An Engineering Perspective, PODC'07.
9 2/11/2021 SC Replication, CRDTs, CALM [Video] Shapiro et al, Conflict-free Replicated Data Types, HAL TR.
Hellerstein et al, Keeping CALM: When Distributed Consistency is Easy, CACM Sep 2020.
Verification Techniques
10 Hoare Logic
Rely-Guarantee		 Chapters 1 & 2 of Mike Gordon's Background Reading on Hoare Logic.
Feng, Local Rely-Guarantee Reasoning, POPL'09.
11 Refinement Proof Technique
Proof automation		 Lynch, Simulation Techniques for Proving Properties of Real-Time Systems, 1993.
Paper Discussions - Distributed Systems Verification
12 Hawblitzel et al, IronFleet: Proving Practical Distributed Systems Correct, SOSP'15.
13 Wilcox et al, Verdi: A Framework for Implementing and Formally Verifying Distributed Systems, PLDI'15.
14 Padon et al, Ivy: Safety Verification by Interactive Generalization, PLDI'16
15 Gleissenthall et al, Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs, POPL'19.
16 Ma et al, I4: Incremental Inference of Inductive Invariants for Verification of Distributed Protocols, SOSP'19.
From Distributed Systems to Distributed Applications
17 Geo-Replication & Replicated Data Types DeCandia et al, Dynamo: Amazon’s Highly Available Key-Value Store, SOSP'07.
Shapiro et al, Conflict-free Replicated Data Types, 2011.
Kaki et al, Version Control is For Your Data Too, SNAPL'19.
Paper Discussions - Distributed Applications Verification
18 Sivaramakrishnan et al, Declarative Programming over Eventually Consistent Data Stores, PLDI'15.
19 Bailis et al, Probabilistically Bounded Staleness for Practical Partial Quorums, VLDB'12.
20 1. Nakamoto, Bitcoin: A Peer-to-Peer Electronic Cash System, 2008
2. Garay et al, The Bitcoin Backbone Protocol: Analysis and Applications, EUROCRYPT'15.
21 Wood, Ethereum: A Secure Decentralised Generalised Transaction Ledger, 2014 Ethereum White Paper
22 Brent et al, Ethainter: A Smart Contract Security Analyzer for Composite Vulnerabilities, PLDI'20. Li et al, A Survey on the Security of Blockchain Systems, arXiv:1802.06993.
23 1. Bonneau et al, Coda: Decentralized Cryptocurrency at Scale, 2018.
2. Meckler, Snarky: A High-Level Language for Verifiable Computation, 2018.
24 Gilad et al, Algorand: Scaling Byzantine Agreements for Cryptocurrencies, SOSP'17.