Course Description

The EducationPage is the `official' web-page for this course and has schedule information. This page provides a longer description.

Contents

Program analysis is the activitity that gives a programmer information about his program. Is it type correct? Does every variable obtain a value before I use it? Are all parts of the program I wrote accessible? Is the value assigned to this variable ever used? The first of these questions is answered in detail in Implementation Of Programming Languages. What distinguished the other three analyses from the first one, is that the answers are usually approximative in the sense that to always, and automatically, obtain a complete and correct answer is theoretically impossible. There various ways to cope with this fact, each way giving rise to courses in our curriculum: Type Systems and Implementation Of Programming Languages cope by restricting the set of allowed programs, Program Verification by allowing interaction with the person doing the analysis (although as little of that as possible), while this course takes the approach that the outcomes of an analysis may not be the best possible, but that in many cases they will be good enough.

After shortly digressing to the computability issues responsible, this course continues to investigate the following subjects

1. Dataflow analysis: for a small imperative language we consider how data may flow through the programs, by looking closely at a number of analyses, such as liveness analysis (i.e., will the value of a variable be used in the future). After developing the general framework of monotone frameworks, we add procedures later on.
2. Control flow analysis: to be able to analyze higher-order functional language in a similar way, we first have to solve the dynamic dispatch problem, determining which functions in the program can be applied where. At the end we consider how to combine this with the data flow analysis of the first part of the course.
3. Abstract interpretation: a general approach to program analysis was developed by the Cousots a number of years ago. We investigate their viewpoints on program analysis, which focusses mainly on saving effort by choosing the right kind of analysis (abstraction).
4. Type and effect systems: Chapter 5 of the book comes closest to how we currently do program analysis in our group. I shall also discuss links to our work here at the institute which is part of the Top project.

An important aspect in program analysis to be sure that all the computed answers are sound (safe, correct). Usually this means that we have some obligation to prove for the formulated analysis. This type of proof is part of the course as well.

Along the way various subjects are introduced as necessary, e.g.

1. lattice theory
2. operational semantics
3. computability theory

Form

On average you may expect four hours of lecture and four hours of assisted practical work per week. These are not distributed uniformly over the course period: at the beginning there are more lectures, in later weeks more time should be devoted to the practical assignments.

There is no examination. Instead the student should complete four assignments, which may be either programming assignments or written assignments. Here is a list of the assignments for this year. The practical work sessions take place in a combi-room, so that the student may choose to work on either a written or a programming assignment.

Grade assesment

Grading procedure

The final grade consists of a weighted average of all the assignments to be computed as follows

• 40% for the programming assignment
• 20% for the first two written assignments
• 10% for the final two written assignments

subject to the condition that none of the grades is lower than 4.0. You have passed the course if the average is 5.5 or higher, and if you pass the short oral examination (new this year), which is to make sure that you have indeed learned enough from doing the assignments.

For the written assignments, please do not think that handing in all the correct answers gives you the best possible grade: I shall also look at your argumentation, the elegance of your computations and proofs, clarity and so on.

If you did a previous incarnation of this course, please consult the lecturer, Jurriaan Hage.