CS 643 Formal Verification of Software
Formal systems for specification and verification of software; review of the first-order predicate calculus; abstract data types, formal specification, preconditions, postconditions, invariants, predicate transformers, proofs of correctness, and partial and total correctness; correctness for assignments, alternatives, iterations, and procedure calls. Tools for deductive verification, model checking, and analysis of specifications and models.