Schedule
Time: MW 2:00-3:20pm (Jan 26 - May 20)
Location: NCS 115
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, note NOT CS account, to access. Please don’t spam with permission requests.)
- Jan 26, Introduction
- Jan 28, Memory-related bugs: Introduction
- Feb 2, Rust basics: Ownership and borrowing
- Feb 4, Rust basics: Data types and collections
- Feb 9, Rust basics: Error handling (Result, Option) and pattern matching
- Feb 11, Rust basics: Traits, generics, and lifetimes
- Feb 16, Rust basics: Concurrency and async basics
- Feb 18, Raft
- Feb 23, Raft (cont)
- Feb 25, Verus mechanics
- Mar 2, Recursion, loop invariants, specification
- Mar 4, State machines and behaviors
- Mar 9, State machines and proving properties
- Mar 11, JNF, Inductive invariants
- Mar 16, Spring break
- Mar 18, Spring break
- Mar 23, Inductive invariants, Crawler 2
- Mar 25, Leader election demo
- Mar 30, Leader election (cont), Distributed systems
- Apr 1, Refinement
- Apr 6, Paxos
- Apr 8, Paxos (cont)
- Apr 13, Asynchronous specs
- Apr 15, Application correspondence, triggers
- Apr 20, Cross-host concurrency
- Apr 22, Multi-level refinement
- Apr 27, More formal methods
- Apr 29, Case study: IronFleet
- May 4, Homework framework
Breaks:
- Spring Break Monday, March 16 - Sunday, March 22