Automatic Program Analysis
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 [[Ipt.WebHome][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: [[Ts.WebHome][Type Systems]] and [[Ipt.WebHome][Implementation Of Programming Languages]] cope by restricting the set of allowed programs, [[Pv.WebHome][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. 1 _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. 1 _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). 1 _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 [[Center.Top][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 1 operational semantics 1 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. [[CourseAssignments][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, [[Hage.WebHome][Jurriaan Hage]].