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
- some software horror stories
- more software disasters
- introduction to abstract interpretation, and more in POPL79, here, and more informally here
- Abstract interpretation: a semantics-based tool for program analysis by Jones and Nielson.
- Principles of Program Analysis (book)
- practical success stories: ASTREE SLAM
- cool related projects: TVLA SLAyer Terminator SAFE
- industry: AbsInt Coverity GrammaTech Parasoft Klocwork