CS 5160
Formal Verification
An introduction to formal verification, focusing on correctness of functional and imperative programs relative to mathematical specifications. Topics include computer-assisted theorem proving, logic, programming language semantics, and verification of algorithms and data structures. Assignments involve extensive use of a proof assistant to develop and check proofs.
Topics
- Apply propositional and predicate logic, including constructive and classical reasoning, to reason about programs.
- Explain the Curry-Howard correspondence between proofs and programs, including the interpretation of proof checking as type checking.
- Formulate programs and formal specifications in a type-theoretic framework.
- Construct machine-checked proofs of theorems.
- Design, implement, and verify functional data structures and algorithms, producing implementations together with proofs of correctness.
Official roster learning outcomes
Prerequisites & course information
background equivalent to: CS 3110; CS 2110; CS 2800.
Sources
- Course catalogue ↗2026-2027
- Catalogue entry ↗
Catalogue variants
- Formal Verification · 4.0 · Graduate