MondayTuesday WednesdayThursday Friday
aug 31
Reg Day
sep 1
LEC 1 (nz): Introduction, slides
Preparation: Install class software
Assignment: Basics homework
sep 2 sep 3
LEC 2 (bl): Specifications
Preparation: Read Formal methods at Amazon; do reading questions
Homework due: Basics
Assignment: Induction homework and Lists homework
sep 4
sep 7
Labor day
sep 8
LEC 3 (nz): Coq; Refinement and Hoare logic
Preparation: Read Spec.Proc and Spec.Abstraction
Homework due: Induction and Lists
Assignment: Lab 0: Warmup and Lab 1: StatDB
sep 9 sep 10
LEC 4 (nz): Security
Preparation: Read Everest; do reading questions
sep 11
sep 14 sep 15
LEC 5 (bl): Refinement
Preparation: Read Abstraction Functions and invariants and Generalizing Abstraction Functions; do reading questions
sep 16 sep 17
LEC 6 (nz): Compiler correctness
Preparation: Read CompCert, note, and STACK; do reading questions
Assignment: Lab 2: Remapped disk
sep 18
DUE: Lab 0A
sep 21 sep 22
LEC 7: Recitation on abstraction relations
sep 23 sep 24
LEC 8 (nz): File system specs
Preparation: Read SibylFS; do reading questions
sep 25
DUE: Lab 0B
sep 28 sep 29
LEC 9 (nz): Separation Logic
Preparation: Read Separation Logic; do reading questions
sep 30 oct 1
LEC 10 (nz): File system crash safety
Preparation: Read FSCQ; do reading questions
Assignment: Lab 3: Logging
oct 2
DUE: Lab 1
oct 5 oct 6
LEC 11: Recitation on Lab 3
oct 7 oct 8
LEC 12 (bl): Bug finding
Preparation: Read about static analysis at Google and Facebook; do reading questions
oct 9
DUE: Lab 2A
oct 12
Columbus Day
oct 13
Monday schedule
oct 14 oct 15
LEC 13 (nz): Shared memory
Preparation: Read x86-TSO; do reading questions
oct 16
DUE: Lab 2B
oct 19 oct 20
LEC 14 (nz): Concurrency
Preparation: Read TSVD; do reading questions
oct 21 oct 22
LEC 15 (bl): Specifying concurrency
Preparation: Read Concurrency handout; do reading questions
Assignment: Lab 4: Replicated Disk
oct 23
DUE: Lab 3A
oct 26 oct 27
LEC 16 (nz): Movers for concurrency
Preparation: Read Armada; do reading questions
oct 28 oct 29
LEC 17 (tc): Concurrency using Iris
Preparation: Read A brief introduction to Iris; do reading questions
oct 30
DUE: Lab 3B
nov 2 nov 3
LEC 18 (nz): Distributed systems
Preparation: Read IronFleet; do reading questions
nov 4 nov 5
LEC 19 (nz): Protocol invariant inference
Preparation: Read I4; do reading questions
nov 6
DUE: Lab 4A
nov 9 nov 10
LEC 20: Recitation on Lab 4
nov 11
Veteran's Day
nov 12
LEC 21 (nz): Network verification
Preparation: Read Verified Network Controllers; do reading questions
nov 13
DUE: Lab 4B
nov 16 nov 17
LEC 22 (nz): Bugs in verified systems
Preparation: Read Empirical study; do reading questions
nov 18
nov 19
LEC 23 (bl): Distributed system security
Preparation: Read Komodo; do reading questions
nov 20
DUE: Lab 4C
nov 23
Thanksgiving break
nov 24
Thanksgiving break
nov 25
Thanksgiving break
nov 26
Thanksgiving break
nov 27
Thanksgiving break
nov 30 dec 1
LEC 24 (nz): Non-interference
Preparation: Read CertiKOS; do reading questions
dec 2 dec 3
LEC 25 (nz): Push-button verification
Preparation: Read Serval; do reading questions
dec 4
DUE: Lab 4D
dec 7 dec 8
LEC 26 (nz): Proofs and security
Preparation: Read Fine Print and Side Effects of Proofs; do reading questions
dec 9
Last day of classes
dec 10 dec 11

Questions or comments regarding 6.826? Contact us on Piazza or send e-mail to the 6.826 staff at

Creative Commons License