This page describes the organization of the course and gives access to the course slides and material.
The course is presented (in French) on the M2-6 page on the MPRI site.
The course takes place on Thursday, from 8:45 to 11:45, at University Paris Cité. It takes place in Sophie Germain Building, room 1004, except for the first session, which takes place in room 475F, in the Halle-aux-Farines Building .
The course is organized in two periods of 8 courses each.
The first period will begin on 14 September 2023. The first period will end with a 3-hour written exam on November 30, from 8:45 to 11:45 AM.
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 dates may change, so, please consult this page regularly for updates.
The course slides will be put on-line before or shortly after each course.
Reading materials are provided below, including introductory articles and course notes for the first part of the course.
The courses are accompanied with a suggestion of homework assignments. They consist in course-specific reading assignments, exercises to complete, or experiments to perform. Assignments are not evaluated by the teachers and give no credit: they are for self-evaluation only, to prepare you for the exams. Although optional, it is highly recommended that you complete these assignments.
To complete the theoretical study with implementation, we propose a project (in French).
It is completely optional and not evaluated by the teachers.
First Period
Important: The first lesson takes place in amphitheater 475F in the Halle-aux-Farines Building, 4th floor.
Topics: Course organization; Introduction; Order theory.
Slides:
Assignments:
Important: Staring from Lesson 2, the lessons take place in the Sophie Germain Building, room 1004.
Topics: Semantics and properties.
Slides:
Assignments:
Topics: Non-relational numeric abstract domains.
Slides:
Assignments:
Topics: Relational numeric abstract domains.
Slides:
Assignments:
Topics: Partitioning abstract domains.
Slides:
Assignments:
Topics: Thread-modular static analysis of concurrent programs.
Slides:
Assignments:
Topics: Specific numerical domains.
Slides:
Assignments:
Topics: Termination analysis.
Slides:
Mid-term written exam: on 30 November 2023, from 08:45 to 11:45 AM (3 hours).
See also the former written exams.
Second Period
Topics: Analysis of liveness and CTL properties.
Slides:
Topics: Static analysis for Data Science.
Slides:
Topics: Formal verification of Machine Learning.
Slides:
Topics: Abstract interpretation of mobile systems.
Topics: Memory abstraction.
Topics: Shape analysis abstractions.
Topics: Security analysis.
Final oral exam: 5 March 2024 morning (09:00-12:30) and 7 March 2024 afternoon (13:30-17:00).
The following articles give an taste of the contents and the goal of the course:
Several recent books have been published on Abstract Interpretation:
Course notes are available for the beginning of the course. They cover roughly lessons 1 to 4.
The contents of the later lessons is generally covered in articles. Each course will thus provide a specific bibliography in the course slides, for reference (reading is them is not mandatory).
An example programming project (in French) is available, with associated source code. The goal is to extend a small analyzer for a toy language written in OCaml.
This completely optional project will not be evaluated by the teachers and will not give credit. It is here for students wishing to practice the implementation of some principles seen during the course.
The project is based on a course given at École normle supérieure and at Sorbonne Université.
We will provide here a list of M2 internship proposals related to the course, either in the Antique team at the ENS (Paris), the APR team at Sorbonne Université (Paris), or the SyCoMoRES team (Lille).
The list is updated regularly!
Feel also free to contact directly the teachers for more information and more proposals.