Course Websites

Mathematical models, languages, and methods for software specification, development, and verification. Course Information: Same as ECE 478. 3 undergraduate hours. 3 or 4 graduate hours. Prerequisite: CS 225; one of CS 374, ECE 374 or MATH 414.

Varies by semester.

Be able to do solve problems using structural induction (1,6)

Write code contracts, invariants, and assertions that describe a program's specification formally. (3, 5, 6)

Analyze a program with assertions and find inductive invariants to prove the program correct (1,2, 6)

Given a program with assertions and inductive invariants, be able to derive verification conditions in logic. (1,2,6)

Be able to formulate specifications and properties of structures in logic. (1,2)

Give proofs in Hoare Logic of properties about simple imperative programs. (1,2,6)

Build an abstract interpretation scheme for a program that is sound with respect to given desired properties. (1,2,6)

Formal Logics
Hoare Logic
Abstract Interpretation

Selected Elective.