Part I — Foundations

These chapters explain what it means to prove facts about programs: how specifications are written, how code is connected to logical claims, and how solvers help discharge proof obligations.

• Chapter 1 — Correctness and trust
• Chapter 2 — The limits of testing
• Chapter 3 — Logic and specifications
• Chapter 4 — Hoare logic
• Chapter 5 — Invariants and loops
• Chapter 6 — Ghost reasoning and lemmas
• Chapter 7 — Memory, aliasing, and frame conditions
• Chapter 8 — SMT solvers and automation