— Program Verification

Prerequisites & course information

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. Learning Activities: Lecture 3 hour(s), Discussion 1 hour(s). Enrollment Restriction(s): Open to Graduate Students in Computer Science only. Grade Mode: Letter. Learning Activities: Lecture 3 hour(s), Discussion 1 hour(s). Enrollment Restriction(s): Open to Graduate Students in Computer Science only. Grade Mode: Letter.