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 2022-23.
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.