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 reachable? Is the value assigned to this variable ever used? The first of these questions is answered in detail in Compiler Construction (formerly Implementation Of Programming Languages). What distinguishes 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 are various ways to cope with this fact: by restricting the set of accepted programs (e.g., every decidable type system refuses to accept at least one program that does not go wrong) or, as they do in program verification, by allowing interaction with the person doing the analysis (although as little of that as possible). In static analyses we take the approach that the outcomes of an analysis may not be the best possible, but that in many cases they will be good enough. This allows us to use these analysis in the backends of compilers to silently and always correctly optimise programs, although we may miss some opportunities for optimisation.

In the course I will address various ways of doing program analysis. Typical examples are detection of sign analysis for an imperative language, and soft typing for Python. The examples serve to explain the basic ideas of dataflow analysis (as monotone frameworks), and abstract interpretation, both intraprocedural and interprocedural.

For a functional language, most likely a slightly sugared lambda calculus, we shall consider a modular form of static analysis that can piggyback ride on an already implemented intrinsic type system of the language, by specifying an analysis as a type and effect system. Particular examples are control-flow analysis, dead code analysis, usage analysis, strictness analysis and binding time analysis.

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

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

Form

On average you may expect three 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 students (in pairs) shall work on a few assignments or miniprojects. The students have a large say in what the project may involve.

At the end there may be a short oral examination to make sure that no student piggyback rides on the back of others towards a free passing grade.

Grade assessment

The final grade consists of a weighted average of all assignments and projects. Both project constitute 45 percent of the grade, the remaining 10 percent will be based on your observed participation in the course.

You can only pass the course if none of your grades is lower than 4.0 and the weighted average is 5.5 or higher. There may be an oral examination in the final week to validate your final grade.

For the 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.