Program Verification credit: 3 or

4 Hours

Formal methods for demonstrating correctness and other properties of programs. Invariant assertions; Hoare axiomatics; well-founded orderings for proving termination; structural induction; computational induction; data structures; parallel programs; overview of predicate calculus. 3 undergraduate hours. 3 or 4 graduate hours. Prerequisite: CS 225 ; one of CS 374 , ECE 374 or MATH 414 .