CS 4160

Formal Verification

Course Description

Course information provided by the 2026-2027 Catalog.

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.

Prerequisites CS 3110 or permission of instructor.

Enrollment Information Enrollment limited to: Computer Science majors.

Distribution Requirements (SMR-AS)

Last 4 Terms Offered 2026SP, 2022SP, 2020SP, 2019SP

Learning Outcomes

• 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.

View Enrollment Information