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.

Credits

3

Prerequisite

CPE 600 or CS 600 or CS 392