CS 116: Reasoning about Program Correctness

Caltech Course CS 116 provides an introduction to formal reasoning about correctness of computer programs. We will cover both the theory and the practice of program reasoning, focusing more on the practice.

We will look at representative programming problems and discuss how to verify correctness using automated tools like Dafny and the VCC verifier being used to tackle verification of complex programs such as the Microsoft hypervisor.

Topics include

• writing formal specifications of program behavior
• fundamentals of program reasoning using preconditions, postconditions and loop invariants
• introduction to predicate transformer semantics
• specification and verification of representative examples
• basics of verification condition generation
• theory of "miracles" and programming in a language with miracles

• CS 118: Logic Model Checking, taught by Gerard Holzmann