MondayTuesday WednesdayThursday Friday
sep 2 sep 3
Reg Day
sep 4 sep 5
LEC 1 (nz): Introduction, slides
Preparation: Install class software
Assignment: Basics homework
sep 6
sep 9 sep 10
LEC 2 (bl): Specifications
Preparation: Read Formal methods at Amazon; do reading questions
Homework due: Basics
Assignment: Induction homework
sep 11 sep 12
LEC 3 (nz): Coq
Homework due: Induction
Assignment: Lists homework
Assignment: Lab 0: Warmup
sep 13
sep 16 sep 17
LEC 4 (nz): Refinement and Hoare logic
Preparation: Read Spec.Proc and Spec.Abstraction
Homework due: Lists
Assignment: Lab 1: StatDB
sep 18 sep 19
LEC 5 (bl): Refinement
Preparation: Read Abstraction Functions and invariants and Generalizing Abstraction Functions; do reading questions
sep 20
Student holiday
sep 23 sep 24
LEC 6 (nz): Compiler correctness
Preparation: Read CompCert, note, and STACK; do reading questions
sep 25 sep 26
LEC 7 (tc): Verifiable assembly
Preparation: Read Vale; do reading questions
Assignment: Lab 2: Remapped disk
sep 27
DUE: Lab 0A
sep 30 oct 1
LEC 8 (nz): File system specs
Preparation: Read SibylFS; do reading questions
oct 2 oct 3
LEC 9 (nz): Specifying a high-performance file system
Preparation: Read DFSCQ; do reading questions
Assignment: Lab 3: Logging
oct 4
DUE: Lab 0B
oct 7 oct 8
LEC 10 (bl): Bug finding
Preparation: Read A few billion lines of code later; do reading questions
oct 9 oct 10
LEC 11 (nz): Shared memory
Preparation: Read x86-TSO; do reading questions
oct 11
DUE: Lab 1
oct 14
Columbus Day
oct 15
Columbus Day
oct 16 oct 17
LEC 12 (nz): Concurrency
Preparation: Read Chess; do reading questions
oct 18
DUE: Lab 2A
oct 21 oct 22
LEC 13 (bl): Specifying concurrency
Preparation: Read Concurrency handout; do reading questions
Assignment: Lab 4: Replicated Disk
oct 23 oct 24
LEC 14 (nz): Movers for concurrency
Preparation: Read CSPEC; do reading questions
oct 25
DUE: Lab 2B
oct 28 oct 29
Hacking day
oct 30 oct 31
Hacking day
nov 1
DUE: Lab 3A
nov 4 nov 5
LEC 15 (tc): Concurrency using Iris
Preparation: Read Perennial; do reading questions
nov 6 nov 7
LEC 16 (bl): Distributed systems
Preparation: Read TCP puzzlers and Reliable messages; do reading questions
nov 8
DUE: Lab 3B
nov 11
Veteran's Day
nov 12
LEC 17 (nz): Distributed systems
Preparation: Read IronFleet; do reading questions
nov 13 nov 14
Recitation on Lab 4
nov 15
DUE: Lab 4A
nov 18 nov 19
LEC 18 (nz): Network verification
Preparation: Read Verified Network Controllers; do reading questions
nov 20
nov 21
LEC 19 (nz): Bugs in verified systems
Preparation: Read Empirical study; do reading questions
nov 22
DUE: Lab 4B
nov 25 nov 26
LEC 20 (nz): Isolation
Preparation: Read Hyperkernel; do reading questions
nov 27 nov 28
nov 29
dec 2 dec 3
LEC 21 (nz): Non-interference
Preparation: Read CertiKOS; do reading questions
dec 4 dec 5
LEC 22 (bl): Security
Preparation: Read Komodo; do reading questions
dec 6
DUE: Lab 4C
dec 9 dec 10
LEC 23 (nz): Security
Preparation: Read Everest; do reading questions
dec 11
Last day of classes
DUE: Lab 4D
dec 12 dec 13

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

Creative Commons License