Plans for 02913 ”Advanced Analysis Techniques” (January 2019 – Abstract Interpretation)

·       The course takes place at DTU starting Monday, January 7th and lasts for three weeks.

·       During the first week we meet in 324.261 at 10.00.

·       The topic for January 2019 is Abstract Interpretation
.

·       It is organized by Hanne Riis Nielson and Flemming Nielson.

·       To sign up for the course you should register at DTU Inside or contact the organizers.

·       For formalities please take a look at http://www.kurser.dtu.dk/02913.aspx?menulanguage=en-GB

Motivation

Abstract Interpretation is one of the most general – but perhaps also most difficult – approaches to the static analysis of programs. Pioneered by Patrick and Radhia Cousot in the 1970’s this is a powerful approach to static analysis that requires some mathematical maturity to fully master – and hence is not as generally applied as the power of the techniques would merit.

 

This course will cover the basic concepts of Abstract Interpretation: “A Mundane Approach to Correctness”,  Approximation of Fixed Points”, “ Galois Connections”, “Systematic Design of Galois Connections”, and “Induced Operations” following the presentation in [PPA]

 

In a project you are supposed to apply the methods and techniques to the problem of devising independent attribute based and relational analyses over the integers and to relate these using abstract interpretation. As a minimum should devise a collecting semantics, show how to obtain the detection of signs analysis in [FM] using abstract interpretation, and furthermore show how to obtain the detection of signs analysis in [PA]. Please feel free to add additional steps to the development and to discuss possible difficulties in integrating the interval analysis from [PA] into the development.

 

If you are unfamiliar with detection of signs analyses you may find the systems at FormalMethods.dk helpful to get acquainted with them.

 

Teaching Schedule

Lectures starting at 10.00 for the first few days.

Consultancy a few times a week on the projects.

Reports to be handed in by mail to the teachers no later than Thursday January 24’th at noon.

Oral presentation and exam on Friday January 25’th in the morning.

 

Lecture Materials to be handed out

 

[PPA] Flemming Nielson, Hanne Riis Nielson, Chris HankinPrinciples of Program Analysis: Chapter 4: Abstract Interpretation. [Slides for Chapter 4]. Springer, 2005.

 

[FM] Flemming Nielson, Hanne Riis Nielson: Formal Methods – An Appetizer: Chapter 4: Program Analysis. Springer, 2019.

 

[PA] Flemming Nielson, Hanne Riis Nielson: Program Analysis – An Appetizer: Chapter 5: Analysis of Integers. Manuscript.

 

Additional material to be made available on DTU Inside.