Aim and Scope

In this course you will learn how to reason about programs without running them. You will learn how to establish interesting properties of programs statically (at compile time). For example, showing that a program is not exposed to certain security vulnerabilities.

We will cover a wide range of approaches, from lightweight techniques for automatically verifying simple properties, all the way to automatically proving properties about the shape of a program's heap.

The course will provide theoretical background and hands on experience. During the course you will build your own program analyzer and apply it to real programs.

The course combines several views of software verification --- verification via abstract interpretation, deductive verification, and algorithmic verification (model checking). In the first part of the course, we will survey program analysis and abstract interpretation. In the second part, we will explore deductive verification. Finally, we discuss some practical aspects of applying abstraction in model checking.

Lectures

  • Tuesday 12:30-14:30
  • Thursday 10:30-12:30 (part of the semester)
  • Thursday 10:30-11:30 (recitation, part of the semester)

Course Requirements

  • homework assignments
  • project
  • course notes

Resources