Tue/Thu 1:00 - 2:30

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

Planned topics:

• basics of propositional and first-order logic
• writing logical specifications of intended program behavior
• sequential program reasoning with Hoare logic, using preconditions, postconditions and loop invariants
• relational and predicate-transformer semantics of programs
• using weakest preconditions as hints in developing programs from specifications (programs that are "correct by construction")
• theory of program refinement

Emphasis will be on working with lots of examples, since programming cannot be learned except "by doing". Students will be encouraged to apply methods taught in class by using freely available verification tools to their programs.

Grading will be based on take-home assignments and a class project. There is no assigned textbook; handouts and lecture notes will be given as needed to supplement material taught in class.

CS 116 is a companion course to
CS 118: "Logic Model Checking" (taught by Gerard Holzmann, Winter), and
CS 119: "Testing and Monitoring" (taught by Alex Groce and Klaus Havelund, Spring)