Program Analysis

G22.3033-016
Monday, 5:00-6:50 PM
Room 101 WWH
Amir Pnueli

Reaching Me

Amir Pnueli

Course Description

This interdisciplinary course lies on the border between Compiler Techniques and Program Verification. It introduces methods intended to guarantee with very high confidence that an industrial-size program meets its specification and can never hurt the environment in which it is run.

The methods considered extend the compiler technology of data- and control-flow analysis and type checking, by paying more attention to the accumulation and utilization of program invariants.

The verification field contributes to this area the techniques of abstract interpretation, predicate abstraction, and static analysis. These techniques will be introduced and studied as the foundation for program analysis.

The area of program analysis is gaining more interest and attention also from the industrial sector, as illustrated by the recent adoption by Microsoft of their own program-analysis tool SLAM for verifying the safety of device drivers which are contributed to Windows by the equipment manufacturers.

Prerequisites: Some background in algorithm design, familiarity with the language of first-order logic, and knowledge of compiler construction techniques.

Course requirements: Assignments and a term project.

Textbooks:
Recommended: Principles of Program Analysis, by Flemming Nielson, Hanne Riis Nielson, Chris Hankin, Springer-Verlag.

Class Presentations

TLV Resources

Assignments