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

Revisions in last 6 years	Approximately when revision was done	Reason for revision
Each semester the instructor has chosen difference emphases in order to introduce and interest the students in recent research topics.		This helos to serve learning outcome (h) recognition of the need for and an ability to engage in continuing professional development

Selected Elective.