Reasoning about Program Correctness
9 units (3-0-6) |
Prerequisites: CS 1 or equivalent.
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 2021-2022
The online version of the Caltech Catalog is provided as a convenience; however, the printed version is the only
authoritative source of information about course offerings, option requirements, graduation requirements,
and other important topics.