CS 4160 - [Formal Verification]

(SMR-AS)

Spring. Not offered: 2024-2025. Next offered: 2025-2026. 4 credits. Student option grading.

Prerequisite: CS 3110 or permission of instructor. Students are expected to be proficient with programming (e.g. CS 2110), and proof (e.g. CS 2800 or a mathematics course numbered 3000 or above). Co-meets with CS 5160.

M. Clarkson.

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.