CS 476
Program Verification

Credit:  3 or 4 hours.


Examines formal methods for demonstrating correctness and other properties of programs; includes an overview of predicate calculus. Topics include: invariant assertions, Hoare axiomatics, well-founded orderings for proving termination, structural induction, computational induction, data structures, and parallel programs. 3 undergraduate hours. 3 or 4 graduate hours. Prerequisite: CS 225; CS 273 or MATH 414.