Program Verification

Catalog description

Course Description: Methods of proving correctness of programs with respect to formal specifications, with attention to those suited for employing automated deduction. Logic background, symbolic execution, techniques suited to iterative programming, methods from denotational semantics, termination, dynamic logic and proofs of concurrent programs.