CS 5160

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 background equivalent to: CS 3110; CS 2110; CS 2800.

Enrollment Information Enrollment limited to: Computer Science (CS) Master of Engineering (M.Eng.) students.

Last 4 Terms Offered 2026SP, 2022SP

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