Abstract Interpretation

News

The course homepage will be updated continuously. Please check back regularly.

Recent updates:

Jun 8, 2011: Updated the time and location for the oral exams.
May 31, 2011: Uploaded a tentative exam schedule.
May 24, 2011: Uploaded slides from today's lecture and a link to an earlier (optional) ASTRÉE paper from 2002.
May 21, 2011: Added a link to the mathpartir package under LaTeX resources.
May 17, 2011: Uploaded slides from today's lecture.
May 16, 2011: Uploaded a revised version of week 4 slides, correcting argument \S# to S# on slide 48.
May 11, 2011: Uploaded (slightly revised) slides, incl. a few on constraint extraction (mostly in ASCII, with apologies). Also added a link to Cousot-Cousot:ICCL94.

Description

The course provides a basic knowledge about abstract interpretation. In the classical framework the execution of programs is modelled by a transition system. The space of possible executions (the collecting semantics) is then systematically over-approximated through Galois connections.

We will study both the theoretical, mathematical foundation, as well as implement the resulting analyses in practice as executable abstract interpreters.

The official course description

Time and place

Lectures: Tuesday 12.15-15.00, in 5523.131, i.e., room 131 in IT-huset / Incuba Science Park.

Lecturer

Jan Midtgaard <>

Please do not hesitate to contact me in case of comments or questions regarding the course.

Course Plan (subject to rearrangements)

Lecture	Topic	Course Material	Handins
Tue April 5	Course intro + Basic concepts of abstract interpretation + OCaml intro	Cousot-Cousot:BIS04 Slides from the lecture Code from the lecture: initialsteps.ml transsys.ml	Handin 1 Deadline: April 12
Tue April 12	Operational semantics: transition system semantics for 3CM, CPS, IMP and JVM-like bytecodes	Plotkin:TR81, chap.1 Slides from the lecture Flanagan-al:PLDI93 (optional) Siveroni:JLAP04 (optional)	No handin
Tue April 19	No lecture - Lecture postponed until after Easter (despite the official teaching calendar)
Tue April 26	Concepts of abstract interpretation I Calculating a three counter machine analysis I	Cousot-Cousot:JLP92, p.1-18 (Sec.7-10 optional) Slides from the lecture Calculation of 3 counter machine analysis, part 1 Implementation of Plotkin's 3 counter machine	Handin 2 Deadline: May 3
Tue May 3	Concepts of abstract interpretation II Calculating a three counter machine analysis II	Cousot-Cousot:JLP92, p.18-39 (Sec.7-10 optional) Slides from the lecture Calculation of 3 counter machine analysis, part 2 Calculation of missing operators	No handin
Tue May 10	Numeric and structural abstractions	Miné:thesis, Sec. 2.4.5 - 2.5 Deutsch:POPL90 (note: link is only accessible from Campus or over VPN), Sec. 2 (the rest is optional) Slides from the lecture Link: A graphical overview of a number of numeric abstractions Cousot-Cousot:ICCL94 (optional,however a treasure chest of Galois connections)	Handin 3 Deadline: May 17
Tue May 17	Case studies: Control-flow analysis by abstract interpretation and Abstract Debugging of Higher-Order Imperative Languages	Midtgaard-Jensen:ICFP09 Bourdoncle:PLDI93 Slides from the lecture	Project description Deadline: May 24 at 12:00
Tue May 24	Case studies: Context-Sensitive Analysis of Obfuscated x86 Executables, and The ASTRÉE Static Analyzer	Lakhotia-al:PEPM10 Blanchet-al:PLDI03 Slides from the lecture Slides from Lakhotia-al's PEPM'10 presentation Slides from Blanchet-al's PLDI'03 presentation Blanchet-al:Jones-festschrift02 (optional)	No handin

OCaml resources

LaTeX resources

A brief guide on typesetting AbsInt handins in LaTeX.
The galois package (also included in most LaTeX distributions)
The mathpartir package (for typesetting inference rules nicely)
Lars Madsen's LaTeX book 'Introduktion til LaTeX' (in Danish).

Project

Please try to come up with an idea for a course project yourself. This is an opportunity for you to apply your newly acquired skills to a transition system of your choice. Note: it doesn't need to be a semantics for a programming languages. The measure of success will be whether you can apply the abstract interpretation principles and techniques acquired in the course. You're welcome to do an individual course project, or to form project groups of 2-3 participants.

Please contact me with your project idea (for pointers to get you started, moral support, etc.).

If everything else fails, here is a few ideas for inspiration:

Interface the 3 counter machine with the PPL or APRON libraries and experiment with some of their numerical abstract domains.
Beef up the 3 counter machine with more instructions, registers, etc., and develop and implement a (non-trivial) analysis of the resulting machine.
Develop and implement forwards/backwards analysis of the 3 counter machine.
Develop and implement a minimal disjunctively-completed analysis of the 3 counter machine.
Implement the CFA from Midtgaard-Jensen:08 by extending the given lexer and parser. Extend it minimally by a numeric abstract domain of your choice.
Implement a (non-trivial) analysis for the imperative core language.
Implement a (non-trivial) analysis of the Integer Java Virtual Machine (IJVM) (or some extension hereof).

Library links for inspiration:

PPL - the Parma Polyhedra Library
APRON - numerical abstract domain library
JavaLib - Java class file parser
...

Paper links (approaching propaganda):

Exam

Dates: June 10 (9:30-12:30), June 17 (13:00-14:00), July 1 (9:30-13:00), all in Turing-230

Here's a tentative exam schedule.

You must have the (bi)weekly hand-ins accepted in order to attend the exam.

Participants will be evaluated on both the course project and a 20-min oral examination (without preparation) after which a combined (7-scale) grade is given.

The best entry to the oral exam is thus a completed/successful project. The oral exam is an opportunity to talk about your project.

AbsInt