Schedule
Time: MW 2:00-3:20pm (Jan 27 - May 9)
Location: Staller 3216
Office hour: MW 1-2pm NCS 351 (Please book a meeting on Google Calendar a day before).
Lecture Schedule:
Lecture notes can be found here. It requires a Stony Brook email to access. Please don’t spam with permission requests.
- Jan 27, Introduction
- Jan 29, Crash course of Rust
- Feb 3, Verus mechanics
- Feb 5, Recursion, loop invariants, specification
- Feb 10, State machines and behaviors
- Feb 12, State machines and proving properties
- Feb 17, JNF, Inductive invariants
- Feb 19, Inductive invariants, Crawler 2
- Feb 24, Leader election demo
- Feb 26, Leader election (cont), Distributed systems
- Mar 3, Refinement
- Mar 5, Paxos
- Mar 10, Paxos (cont)
- Mar 12, Asynchronous specs
- Mar 17, Spring break
- Mar 19, Spring break
- Mar 24, Application correspondence, triggers
- Mar 26, Modules and automation
- Mar 31, Cross-host concurrency
- Apr 2, Multi-level refinement
- Apr 7, Incremental Inference of Inductive Invariants
- Apr 9, Case study: IronFleet
- Apr 14, The future of systems verification
Breaks:
- Spring Break Monday, March 17 - Sunday, March 23
- On average, we will have 1-2 classes cancelled due to my travels.