Monday | Tuesday | Wednesday | Thursday | Friday |
aug 31 Reg Day |
sep 1 LEC 1 (nz): Introduction (boards, video) Preparation: Install class software Assignment: Basics homework |
sep 2 | sep 3 LEC 2 (bl): Specifications (slides, video) Preparation: Formal methods at Amazon Homework due: Basics Assignment: Induction and Lists homework |
sep 4 |
sep 7 Labor day |
sep 8 LEC 3 (nz): Hoare logic (boards, video) Preparation: Read Spec.Proc and Spec.Abstraction Homework due: Induction and Lists Assignment: Logic homework Assignment: Lab 1: StatDB |
sep 9 | sep 10 LEC 4 (bl): Security (video) Homework due: Logic Preparation: Everest |
sep 11 |
sep 14 | sep 15 LEC 5 (bl): Refinement (video) Preparation: Abstraction functions |
sep 16 | sep 17 LEC 6 (nz): Compiler correctness (boards, video) Preparation: CompCert Assignment: Lab 2: Remapped disk |
sep 18 DUE: Lab 1A |
sep 21 | sep 22 LEC 7 (nz): Bug finding (boards, video) Preparation: Static analysis at Google and Facebook |
sep 23 | sep 24 LEC 8 (nz): File system specs (boards, video) Preparation: SibylFS |
sep 25 DUE: Lab 1B |
sep 28 | sep 29 LEC 9 (tc): Separation Logic (whiteboard, video) Preparation: Separation logic Homework due: Summary group 1 |
sep 30 | oct 1 LEC 10 (nz): File system crash safety (boards, video) Preparation: FSCQ |
oct 2 ADD DATE DUE: Lab 2A |
oct 5 | oct 6 LEC 11 (nz): Shared memory (boards, video) Preparation: x86-TSO Homework due: Summary group 2 Assignment: Lab 3: Logging |
oct 7 | oct 8 LEC 12 (nz): Concurrency (boards, video) Preparation: TSVD |
oct 9 DUE: Lab 2B |
oct 12 Indigenous Peoples Day |
oct 13 Monday schedule |
oct 14 | oct 15 LEC 13 (sl): Recitation on Lab 3 (video) |
oct 16 DUE: Lab 3A |
oct 19 | oct 20 LEC 14 (bl): Formal concurrency (video) Preparation: PlusCal Assignment: Lab 4: Replicated Disk |
oct 21 | oct 22 LEC 15 (nz): Movers for concurrency (boards, video) Preparation: Armada |
oct 23 DUE: Lab 3B |
oct 26 | oct 27 LEC 16 (tc): Concurrency using Iris (whiteboard, video) Preparation: Iris |
oct 28 | oct 29 LEC 17 (bl): Distributed systems (video) Preparation: IronFleet Homework due: Summary group 3 |
oct 30 DUE: Lab 3C |
nov 2 | nov 3 LEC 18 (nz): Protocol verification (boards, video) Preparation: I4 |
nov 4 | nov 5 Hacking day |
nov 6 DUE: Lab 4A |
nov 9 | nov 10 LEC 19 (nz): Network verification (boards, video) Preparation: Verified network controllers |
nov 11 Veteran's Day |
nov 12 LEC 20 (nz): Bugs in verified systems (boards, video) Preparation: Empirical study |
nov 13 DUE: Lab 4B |
nov 16 | nov 17 LEC 21 (bl): Distributed system security (video) Preparation: Komodo Homework due: Summary group 4 |
nov 18 DROP DATE |
nov 19 LEC 22 (nz): Non-interference (boards, video) Preparation: CertiKOS |
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 23 (nz): Proofs and security (boards, video) Preparation: Fine Print and Side Effects of Proofs |
dec 2 | dec 3 LEC 24 (xw): Push-button verification (video) Preparation: Serval |
dec 4 DUE: Lab 4D |
dec 7 | dec 8 LEC 25 (bl): Reliability without proofs (video) Preparation: Tony Hoare's paper |
dec 9 Last day of classes Homework due: Summary group 5 |
dec 10 | dec 11 |