Yusuf's Thoughts

Program Verification

1 min read

Program Verification

Lecture notes for the master’s PV course. The course teaches how to formally prove that programs do what their specifications say, using logic, SMT solvers, and Hoare-style reasoning.

Foundations

  1. (y-01) Introduction to Program Verification
  2. (y-02) Propositional Logic
  3. (y-03) First-Order Logic
  4. (y-04) First-Order Theories

Logic & Tools

  1. (y-05) SMT-LIB
  2. (y-06) Boogie and Boostan
  3. (y-07) Relational Semantics
  4. (y-08) Hoare Proof System
  5. (y-09) Ultimate Referee

Data & Nondeterminism

  1. (y-10) Array Theory and Arrays in Boostan
  2. (y-11) Nondeterminism: Havoc and Assume

Automating Verification

  1. (y-12) Control-Flow Graphs
  2. (y-13) Predicate Transformers
  3. (y-14) Bounded Model Checking
  4. (y-15) Correctness via Assert Statements

Advanced Techniques

  1. (y-16) Abstractions and ARG
  2. (y-17) Infeasibility Proofs and CEGAR
  3. (y-18) Trace Abstraction and Automata
  4. (y-19) Constraint-Based Invariant Synthesis

Tools

  • Z3: SMT solver from Microsoft Research.
  • Ultimate Automizer: automated software verifier.
  • Boogaloo: interpreter and symbolic execution tool for Boogie.
  • Ultimate Referee: tool for checking loop invariants.

(y) Return to Notes | (y) Return to Home

19 items under this folder.