| CARVIEW |
Select Language
HTTP/2 301
location: https://rjoshi.org/cs116/
content-length: 233
content-type: text/html; charset=iso-8859-1
date: Mon, 19 Jan 2026 05:10:44 GMT
server: Apache
HTTP/2 200
last-modified: Wed, 20 Sep 2017 12:18:08 GMT
accept-ranges: bytes
vary: Accept-Encoding
content-encoding: gzip
host-header: c2hhcmVkLmJsdWVob3N0LmNvbQ==
content-length: 2145
content-type: text/html
date: Mon, 19 Jan 2026 05:10:44 GMT
server: Apache
Caltech CS 116: Introduction to Program Reasoning
CS 116 is a companion course to
1 - 2:25 p.m.
Annenberg 107
Caltech campus
Email
rjoshi "at" caltech "dot" edu
These web pages use cascading style sheet features for
formatting. You may still browse the text of the site, but for best
results, use a modern CSS-enabled browser.
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 116 is a companion course to
- CS 118: Logic Model Checking, taught by Gerard Holzmann
Logistics
Tue / Thu1 - 2:25 p.m.
Annenberg 107
Caltech campus