# Site

## Pages

- [Page not found](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-isaacboentoro/404/): That page doesn't exist, or it has moved since you last looked
- [Assessment](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-isaacboentoro/assessments/): Every piece of graded work in the course, what it is worth, and when it is due.
- [Comparative verification report](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-isaacboentoro/assessments/comparative-verification-report/): Apply at least two tools from the semester to the same C program and argue which one you'd actually ship
- [Retrofit case study](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-isaacboentoro/assessments/retrofit-case-study/): Verify a small, real C function memory-safe with one tool from the semester, and argue why that tool was the right fit
- [Lectures](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-isaacboentoro/lectures/): What is covered, week by week, and which topics each lecture draws on.
- [Why C has none of this](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-isaacboentoro/lectures/week-01/): C's design tradeoffs — speed, portability, no runtime — and the bug classes that follow from having no memory safety at all
- [What compile-time can even prove](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-isaacboentoro/lectures/week-02/): Undecidability, alias analysis, and the soundness/completeness tradeoff every static memory-safety check has to make
- [Ownership as a foil](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-isaacboentoro/lectures/week-03/): 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
- [Cyclone: region-based memory](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-isaacboentoro/lectures/week-04/): A retrofit that shipped a whole safe dialect of C rather than annotating the existing one — region-based allocation and what it forbids
- [Checked C: bounds without a new language](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-isaacboentoro/lectures/week-05/): Bounds-checked pointer types added to ordinary C, and the spatial-only safety guarantee that buys
- [Separation logic: reasoning about the heap](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-isaacboentoro/lectures/week-06/): 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
- [Frama-C and ACSL: deductive verification](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-isaacboentoro/lectures/week-07/): Annotating real C with ACSL contracts and discharging the resulting proof obligations against the source, not a model of it
- [CompCert: what a proven compiler doesn't promise](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-isaacboentoro/lectures/week-08/): CompCert's formally verified compilation correctness, and the memory-safety question it deliberately leaves to you
- [MISRA-C and industrial static analysis](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-isaacboentoro/lectures/week-09/): What Coverity, the clang static analyzer, and cppcheck actually check for, and how that differs from the formal guarantees of weeks 5–7
- [Academic borrow-checking retrofits for C](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-isaacboentoro/lectures/week-10/): 3C, RefinedC, and the current research push to bring ownership-style reasoning back into C without leaving the language
- [Case study: one CVE, every tool](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-isaacboentoro/lectures/week-11/): 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
- [Synthesis: what's actually landing](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-isaacboentoro/lectures/week-12/): Which of the semester's ideas are shipping in real toolchains today, and the course's closing argument about what that means
- [People](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-isaacboentoro/people/): Who teaches the course, and how to reach them.
- [Dev Okonkwo](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-isaacboentoro/people/dev-okonkwo/): Tutor for the retrofit weeks and the studios. Spent five years on a compiler-hardening team before crossing over to teaching the tools.
- [Marguerite Voss](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-isaacboentoro/people/marguerite-voss/): The founding convenor. Spent a decade proving small C functions correct by hand before deciding it was faster to teach people why that never scales.
- [Policies and support](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-isaacboentoro/policies/): The course-wide rules for late work, extensions, tool-assistance declarations, and getting help.
- [Studio: break a toy checker](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-isaacboentoro/sessions/week-02-break-a-checker/): Hands-on with a deliberately naive alias-analysis pass — find the program it silently gets wrong
- [Studio: annotate a real function in Frama-C](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-isaacboentoro/sessions/week-07-annotate-frama-c/): Write ACSL contracts for a small, real C function and get Frama-C's WP plugin to actually discharge the proof
- [Studio: reproduce the CVE triage](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-isaacboentoro/sessions/week-11-cve-case-study/): In groups, run a second real CVE through the same tool comparison the lecture just demonstrated