E0 227 Program Analysis and Verification

Instructors: Deepak D'Souza, Aditya Nori, and Sriram Rajamani.

Program verification has become an exciting discipline that combines theory and practice. From a theoretical perspective, the meaning of a computer program, and automatically proving programs correct have been the subject of deep investigation in several sub-disciplines of computer science, and they have given rise to several approaches such as program analysis, theorem proving, model checking and abstract interpretation.

From a practical perspective, commercial software development companies are beginning to use various kinds of program verifiers (and bug finders) in their day-to-day development processes.

We will assume that students have exposure to programming, and some basic knowledge in logic, automata theory, and formal languages. However, no prior knowledge of program verification or analyses is assumed.

This course will introduce entering graduate students to the theory and practice of program analysis. Side by side, we will teach theory, and through a series of projects, we will build practical program verification tools (by extending and experimenting with publicly available verification tools).