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.
Available fall 2006