MPRI M2-6 Course, year 2012-2013

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

Organization

The course takes place on Friday, from 8:45 to 11:45, at the ENS, in room U/V.

The course is organized in two periods of 8 courses. The first period is from Friday 21 September 2012 to Friday 23 November 2012 and is followed by a written exam. The second period is from Friday 14 December 2012 to Friday 22 Ferbuary 2013 and is followed by 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

You will find here the provisional course plan and the slides. These will be updated progressively.

First Period

• Lesson 1: Friday 21 September 2012, by Antoine Miné.
  • informal introduction to static analysis by abstract interpretation;
  • mathematical notions: partial orders, lattices, fixpoints (up to slide 35);
  • numerical abstract domains: applications, syntax, concrete semantics (up to slide 31).
• Lesson 2: Friday 28 September 2012, by Antoine Miné.
  • follow up on mathematical notions: Galois connections (from slide 36 to the end);
  • follow up on numerical abstract domains: abstraction, non-relational domains (from slide 32 to the end).
• Lesson 3: Friday 5 October 2012, by Antoine Miné.
  • relational numerical abstract domains.
• Lesson 4: Friday 12 October 2012, by Xavier Rival
  • semantics of programs and semantic properties.
• No course on Friday 19 October 2012.
• Lesson 5: Friday 26 October 2012, by Jérôme Feret
  • static analysis of digital filters;
  • the arithmetic-geometric progression abstract domain.
• Lesson 6: Friday 2 November 2012, by Xavier Rival
  • reduced product and partitioning.
• No course on Friday 9 November 2012.
• Lesson 7: Friday 16 November 2012, by Xavier Rival
  • abstraction of memory states.
• Lesson 8: Friday 23 November 2012, by Xavier Rival
  • shape analysis based on separation logic.

Exam: on Friday 7 December 2012. (see also the former exams)

Second Period

• Lesson 9: Friday 14 December 2012, by Matthieu Martel.
  • interprétation abstraite pour la précision numérique : de la détection à la correction d'erreurs.
• Lesson 10: Friday 21 December 2012, by Antoine Miné.
  • analysis of concurrent programs.
• Lesson 11: Friday 11 January 2013, by Jérôme Feret
  • analysis of biological systems 1, and proof of theorems.
• No course on Friday 18 January 2013.
• Lesson 12: Friday 25 January 2013, by Jérôme Feret
  • analysis of biological systems 2.
• Lesson 13: Friday 1 February 2013, by Damien Massé.
  • completeness, policy iteration.
• Lesson 14: Friday 8 February 2013, by Laurent Mauborgne.
  • symbolic abstract domains.
• Lesson 15: Friday 15 February 2013, by Jérôme Feret
  • analysis of mobile systems I (up to slide 71).
• Lesson 16: Friday 22 February 2013, by Jérôme Feret
  • analysis of mobile systems II (from slide 72 to end).

Exam: on Friday 8 March 2013

Former exams

Written exams and their corrections from former years are available on last year's cours.

Internships

You will find below a list of M2 internship proposals related to the course, either in the Abstraction team at the ENS or outside. Feel free to contact directly the teachers for more information and more proposals.

• Compilation optimisante pour la précision numérique, Matthieu Martel, Équipe Projet DALI, laboratoire LIRM, Université de Perpignan.
• Interference abstractions for thread-modular static analyses by abstract interpretation, Antoine Miné, Abstraction Team, Département d'informatique, École normale supérieure, Paris.
• Analyse statique de programme manipulant des structures complexes avec partage, Xavier Rival, Abstraction Team, Département d'informatique, École normale supérieure, Paris.
• Abstraction de relations entre états de la mémoire, Xavier Rival, Abstraction Team, Département d'informatique, École normale supérieure, Paris.

---

Contact: