Programs and Proofs

Course Objectives

This course is about an approach to bringing software engineering up to speed with more traditional engineering disciplines, providing a mathematical foundation for rigorous analysis of realistic computer systems. As civil engineers apply their mathematical canon to reach high certainty that bridges will not fall down, the software engineer should apply a different canon to argue that programs behave properly.

As other engineering disciplines have their computer-aided-design tools, computer science has proof assistants, IDEs for logical arguments and solver-aided languages that automatically verify logical arguments. We will learn how to apply these tools to certify that programs behave as expected.

Specifically, we will look at

  1. Formal logical reasoning about program correctness through
  2. Coq proof assistant, a tool for machine checked mathematical theorem proving and
  3. F*, a general-purpose programming language aimed at program verification

Is this a program verification course?

Yes, but let’s stick to Program Proofs.

Course Contents

Class info

Location: CS26 Time:

Credits

3-1-0-0-8-12

Evaluation Plan

Pre-requisite

CS3100 (only the OCaml parts) or equivalent.

You should feel comfortable with functional programming concepts. If you are able to get through the assignments 1 to 4, you are ready for this course. All the course materials, and assignments are available on the CS3100 website.

I highly recommend that you complete assignments 1 to 4 before the start of this course.

If you are unsure, please come talk to me.