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.
- Lecture 1: Introduction
- Lecture 2: Crash course of Rust
- Lecture 3: Verus mechanics
- Lecture 4: Datatypes, Imperativeland
- Lecture 5: Recursion, loop invariants, specification
- Lecture 6: State machines and behaviors
- Lecture 7: State machines and proving properties
- Lecture 8: JNF, Inductive invariants
- Lecture 9: Inductive invariants, Crawler 2
- Lecture 10: Leader election demo
- Lecture 11: Distributed systems
- Lecture 12: Distributed systems (cont.), Paxos
- Lecture 13: Refinement
- Lecture 14: Asynchronous specs
- Lecture 15: Application correspondence, triggers
- Lecture 16: Modules and automation
- Lecture 17: Cross-host concurrency
- Lecture 18: Multi-level refinement
- Lecture 19: Incremental Inference of Inductive Invariants
- Lecture 20: Case study: IronFleet
- Lecture 20: The future of systems verification
- Lecture 21: Recap of second half
Breaks:
- Spring Break Monday, March 17 - Sunday, March 23
- On average, we will have 1-2 classes cancelled due to my travels.