|
News
The course homepage will be updated continuously. Please check back regularly.
Recent updates:
- Jan 11, 2010:
Added a potential case study, project details and exam details.
- Oct 30, 2009:
Added possible case studies, CodeHawk and SPARROW links.
- Sep 24, 2009:
Added project proposals.
- Sep 23, 2009:
Initial home page created.
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 Shannon-157
Lecturer
Jan Midtgaard
<>
Please do not hesitate to contact me in case of comments or questions
regarding the course.
Course Plan (subject to rearrangements)
Tue
April 13 |
Course intro +
Basic concepts of abstract interpretation |
Cousot-Cousot:BIS04 |
|
Tue
April 20 |
Operational semantics: transition systems |
TBA |
|
Tue
April 27 |
Advanced concepts of abstract interpretation I |
Cousot-Cousot:JLP92 |
|
Tue
May 4 |
Advanced concepts of abstract interpretation II |
Cousot-Cousot:JLP92 |
|
Tue
May 11 |
Numeric abstractions |
Miné:thesis |
|
Tue
May 18 |
Case study: control-flow analysis by abstract interpretation |
Midtgaard-Jensen:ICFP08 |
|
Tue
May 25 |
Case study: (one or more of the following)
C Global Surveyor,
The ASTRÉE Static
Analyzer,
Context-Sensitive Analysis of Obfuscated x86 Executables |
Venet-Brat:PLDI04
Blanchet-al:PLDI03
Lakhotia-al:PEPM10
|
|
Project ideas (ranging from easy to more challenging)
- Implement the CFA from Midtgaard-Jensen:08 by extending the
given lexer and parser. Extend it minimally by an 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).
Alternatively, you are very welcome to make a project of your own
choice applying some of the abstract interpretation principles and
techniques acquired in the course. If you have an idea for such a
project, please contact me (for pointers to get you started etc.).
Library links for inspiration:
- APRON -
numerical abstract domain library
- JavaLib - Java
class file parser
- ...
Paper links (approaching propaganda):
Exam
Date: TBA (between June 4th - July 2nd)
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.
Links
Wikipedia's entry on Abstract Interpretation
Tools based on abstract interpretation:
Similar courses elsewhere:
| 
