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 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 Asynchronous Model of a Distributed System
Failure Modes
Time - Ordering of events, Vector Clocks 		Lamport, Time, Clocks, and the Ordering of Events in a Distributed System, CACM, 1978
3 Coordinated Attack (Two Generals) Problem
FLP Impossibility
CAP & PACELC		 Fischer et al, Impossibility of Distributed Consensus with One Faulty Process, JACM, 1985.
Chandra et al, The Weakest Failure Detector for Solving Consensus, JACM, 1996
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
4 Two-Phase Commit (2PC)
Introduction to TLA+ & PlusCal		 Hillel Wayne's TLA+ & PlusCal Tutorials.
Marc Brooker's Exploring TLA+ with two-phase commit.
Murat Demirbas's TLA+/Pluscal modeling of 2-phase commit transactions.
5 Introduction to TLA+ & PlusCal (contd.)
Liveness and Safety Properties		 Merz, Formal Specification and Verification, Concurrency: the Works of Leslie Lamport, 2019.
6 Paxos Lamport, Paxos Made Simple, ACM SIGACT News, 2001.
Chandra et al, Paxos Made Live: An Engineering Perspective, PODC'07.
7 Paxos (Contd.) Padon et al, Paxos Made EPR: Decidable Reasoning about Distributed Protocols, OOPSLA'17.
Sergey et al, Paxos Consensus, Deconstructed and Abstracted, ESOP'18.
8 Byzantine Generals Problem
BFT Consensus		 Lamport, The Byzantine Generals Problem, TOPLAS'82.
Malkhi et al, Byzantine Quorum Systems, Distributed Computing, 1998. Castro et al, Practical Byzantine Fault Tolerance, OSDI'99.
Verification Techniques
9 Hoare Logic
Rely-Guarantee		 Chapters 1 & 2 of Mike Gordon's Background Reading on Hoare Logic.
Feng, Local Rely-Guarantee Reasoning, POPL'09.
10 Refinement Proof Technique
Proof automation		 Lynch, Simulation Techniques for Proving Properties of Real-Time Systems, 1993.
Paper Discussions - Distributed Systems Verification
11 Hawblitzel et al, IronFleet: Proving Practical Distributed Systems Correct, SOSP'15.
12 Wilcox et al, Verdi: A Framework for Implementing and Formally Verifying Distributed Systems, PLDI'15.
13 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.
14 Padon et al, Reducing Liveness to Safety in First-Order Logic, POPL'18.
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.