This page describes the organization of the course and gives access to the course slides.
The course is presented in the M2-6 page on the MPRI site.
The course is organized in two periods of 8 courses each. The first period will begin on the 17 September 2014. The first period will end with a 3-hour written exam on the 3 December 2014 (usual room and hours). The second period will end with an oral exam. The oral exam consists in the presentation of a research article; the list of articles will be provided a few weeks before the exam.
You will find here the provisional course plan. The course plan will be updated progressively and the slides of the courses will be put on-line before or shortly after each course, so, please consult this page regularly.
Courses are accompanied with a suggestion of homework assignments.
Assignments are not evaluated by the teachers and give no credit: they are for self-evaluation only, to prepare you for the exams.
Assignments may consist in reading assignments, exercises to complete, or experiments to perform.
It is highly recommended that you perform the suggested assignments.
Topics: Course organization; Introduction; Order theory.
Topics: State and traces semantics; State and trace properties.
Slides: 03: program semantics (updated on 24/09/2014).
Topics: Non-relational numerical abstract domains.
Slides: 04: non-relational numerical domains (updated on 01/10/2014).
Topics: Relational numerical abstract domains.
Slides: 05: relational numerical domains (updated on 08/10/2014).
Topics: Inferring ranking functions for termination; Non-linear and floating-point abstractions.
Slides: 06: non-linear and floating-point abstractions (updated on 15/10/2014), 07: automatic inference of ranking functions by abstract interpretation.
Topics: Partitioning abstractions.
Slides: 08: partitioning abstractions
Topics: Domain-specific numerical abstract domains.
Topics: Analysis of Concurrent Programs.
Slides: 11: static analysis of concurrent programs (updated on 13/11/2014).
No assignment: to prepare for the written exam, review the previous assignments and the former written exams.
Written exam: on 3 December 2014. (see also the former written exams)
Topics: Abstraction of memory states.
Slides: 12: Memory Abstraction 1.
Topics: Shape analysis based on separation logic.
Topics: Static analysis of mobile systems (semantics).
Topics: Static analysis of mobile systems (abstraction).
Topics: Program transformations as abstract interpretations.
Topics: The Astrée static analyzer: Abstract Interpretation in practice.
Topics: Static analysis of biological systems (qualitative abstractions).
Topics: Static analysis of biological systems (quantitative abstractions).
Oral exam: on 11 March 2015.
The following articles give an taste of the contents and the goal of the course:
Additionally, a course-specific bibliography is provided in the course slides (for reference; reading is not mandatory).
There is currently no reference book for the course.
You will find below a list of M2 internship proposals related to the course, either in the Abstraction team at the ENS or outside. The list will be updated regularly. Feel free to contact directly the teachers for more information and more proposals.