| |
Apr 25, 2024
|
|
|
|
|
CS 5201 - Software Verification
A course on programming languages and software verification, with hands-on exercise in an interactive theorem prover such as Coq. Topics may include, but are not limited to: logic; functional programming; inductive datatypes, recursion, and structural induction; operational, denotational, and axiomatic semantics; simply typed lambda calculus; polymorphic lambda calculus; type systems and type-checking.
Requisites:
Credit Hours: 3
Repeat/Retake Information: May not be retaken.
Lecture/Lab Hours: 3.0 lecture
Grades: Eligible Grades: A-F,WP,WF,WN,FN,AU,I
Learning Outcomes:
- Students will be able to apply principles of mathematics and computing such as induction to prove properties of programs written in a functional programming language.
- Students will be able to analyze the type system and operational semantics of a small imperative language to prove metatheoretic properties like type soundness.
- Students will be able to analyze a program to identify specifications such as Hoare-logic pre- and post-conditions that capture the program’s expected behavior.
- Students will be able to use an interactive theorem prover to construct a computer-checked proof of type soundness for a small arithmetic expression language.
- Students will be able to use an interactive theorem prover or some other formal methods tool to reason about a software system of their choosing, in the context of an open-ended final project.
Add to Portfolio (opens a new window)
|
|
