C S 430
Download as PDF
Formal Verification
Course Description
Introduction to mathematical formalization and techniques to rigorously establish properties of data structures, functions, and whole programs, including imperative features. Students use a proof assistant embedding several languages including an advanced functional
language.
language.
When Taught
Fall
Min
3
Fixed/Max
3
Fixed
3
Fixed
0
Title
Formalism Design
Learning Outcome
Compare and contrast the purely functional, logical, and embedded logic methods of definition and articulate the consequences of a particular method on a concept.
Title
Algebraic Properties
Learning Outcome
State and prove essential algebraic properties of mathematical operations such as commutativity, associativity, and idempotency.
Title
Theory Design
Learning Outcome
Recognize, produce, and apply metatheoretical properties such as soundness, completeness, and congruence.
Title
Semantics Design
Learning Outcome
Express semantics in operational, denotational, and axiomatic formulations and articulate the relative advantages of each.
Title
Verification Mindset
Learning Outcome
Conceive of and express formal correctness properties of systems without a reference implementation.
Title
Dependently-Typed Programming
Learning Outcome
Express and prove properties about programs using the most advanced extant type systems.
