CS 116 - Reasoning about Program Correctness

This course presents the use of logic and formal reasoning to prove the correctness of sequential and concurrent programs. Topics in logic include propositional logic, basics of first-order logic, and the use of logic notations for specifying programs. The course presents a programming notation and its formal semantics, Hoare logic and its use in proving program correctness, predicate transformers and weakest preconditions, and fixed-point theory and its application to proofs of programs. Not offered 2025-26.