Fall 2020

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