What is covered, week by week, and which topics each lecture draws on.

Every lecture the course claims to run gets a dated page and a teaching-team reference. A course decides how many lectures it needs; one of them carries a real deck. related: connects lectures to the sessions and assessments they feed.

Why C has none of this

C's design tradeoffs — speed, portability, no runtime — and the bug classes that follow from having no memory safety at all

Week 1 · 22 February 2027

What compile-time can even prove

Undecidability, alias analysis, and the soundness/completeness tradeoff every static memory-safety check has to make

Week 2 · 1 March 2027

Ownership as a foil

Rust's borrow checker as the design target every C retrofit in this course gets measured against, even though it isn't itself a C tool

Week 3 · 8 March 2027

Cyclone: region-based memory

A retrofit that shipped a whole safe dialect of C rather than annotating the existing one — region-based allocation and what it forbids

Week 4 · 15 March 2027

Checked C: bounds without a new language

Bounds-checked pointer types added to ordinary C, and the spatial-only safety guarantee that buys

Week 5 · 22 March 2027

Separation logic: reasoning about the heap

The theory that makes it possible to talk about disjoint ownership of heap memory at all, ahead of two weeks that lean on it directly

Week 6 · 29 March 2027

Frama-C and ACSL: deductive verification

Annotating real C with ACSL contracts and discharging the resulting proof obligations against the source, not a model of it

Week 7 · 5 April 2027

CompCert: what a proven compiler doesn't promise

CompCert's formally verified compilation correctness, and the memory-safety question it deliberately leaves to you

Week 8 · 12 April 2027

MISRA-C and industrial static analysis

What Coverity, the clang static analyzer, and cppcheck actually check for, and how that differs from the formal guarantees of weeks 5–7

Week 9 · 19 April 2027

Academic borrow-checking retrofits for C

3C, RefinedC, and the current research push to bring ownership-style reasoning back into C without leaving the language

Week 10 · 26 April 2027

Case study: one CVE, every tool

A real use-after-free CVE run through several of the semester's tools — what each catches, what each misses, and what each cost to try

Week 11 · 3 May 2027

Synthesis: what's actually landing

Which of the semester's ideas are shipping in real toolchains today, and the course's closing argument about what that means

Week 12 · 10 May 2027