everything.study
CMPUT 664

Topics in Software Engineering

3 units

Fall 2026 · Formal Verification: Topics in Software Engineering

Topics

  • SAT and SMT solving
  • Hoare logic and verification conditions
  • Loop invariants
  • Modular verification with Dafny
  • Interactive theorem proving with Lean
  • Inductive and recursive proofs
  • Proof engineering and automation

Readings

  • Aaron R. Bradley and Zohar Manna. The Calculus of Computation: Decision Procedures with Applications to Verification. Springer, 2007.
    recommended
  • Daniel Kroening and Ofer Strichman. Decision Procedures: An Algorithmic Point of View. Springer, 2016.
    recommended
  • Theorem Proving in Lean 4.
    unspecified
Sources