M2-6: Abstract interpretation: application to verification and static analysis

This page describes the organization of the course and gives access to the course slides and material.

The course is presented on the M2-6 page on the MPRI site.

Organization

The course takes place on Wednesday, from 12:45 to 15:45, at University Paris 7, Sophie Germain Building, room 1014.

The course is organized in two periods of 8 courses each.

The first period will begin on 11 September 2019. The first period will end with a 3-hour written exam.

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.

Syllabus, course slides, and assignments

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 course notes for the first part of the course.

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 also propose an implementation project. It is also optional and not evaluated by the teachers.

First Period



Written exam: on 27 November 2019.
(see also the former written exams)


Second Period


Oral exam: on 26 February 2020 and 4 March 2020.

Reading material

Course notes are available. They cover mainly lessons 1 to 4.

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).

Optional project

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é.

Former written exams

Internship proposals

We will provide a list of M2 internship proposals related to the course, either in the Abstraction team at the ENS or the APR team at Sorbonne Université. The list will be updated regularly. Feel free to contact directly the teachers for more information and more proposals.






Contact: