Monday, 5:00-6:50 PM
Room 101 WWH
- phone: (212) 998-3225
- office: WWH, Room 505
- office hours: Monday 2:00-4:00 PM, or by appointment
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
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
Some background in algorithm design, familiarity with the language of
first-order logic, and knowledge of compiler construction techniques.
Assignments and a term project.
Recommended: Principles of Program Analysis, by Flemming Nielson,
Hanne Riis Nielson, Chris Hankin, Springer-Verlag.
Lecture 1 -- Jan. 26, 2004:
Lecture 2 -- Feb. 2, 2004:
Lecture 3 -- Feb. 9,23, 2004:
Lecture 4 -- March 1, 2004:
Lecture 5 -- March 8, 2004:
Lecture 6 -- March 22, 2004:
Lecture 7 -- April 5, 2004:
Lecture 8 -- April 12, 2004:
Lecture 10 -- April 26, 2004: