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 Dafny and the Stainless verifier for (a subset of) the Scala programming language.

Topics include

• writing formal specifications of program behavior
• fundamentals of program reasoning using preconditions, postconditions and loop invariants
• introduction to program semantics using predicate transformers
• specification and verification of representative examples
• a brief overview of SAT and SMT solving
• fundamentals of verification condition generation for automated proofs
• reasoning about object-oriented programs

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