MPRI M2-6 Course, year 2013-2014

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. The course is presented in the M2-6 page on the MPRI site.

New: The list of internship proposals has been updated.

Organization

The course takes place on Friday, from 8:45 to 11:45, at University Paris 7, Sophie Germain Building, Room 1009 (access map, local copy).

The course is organized in two periods of 8 courses. The first period is from 20 September 2013 to 15 November 2013 and is followed by a written exam on 6 December 2013. The second period is from 13 December 2013 to 21 February 2014 and is followed by an oral exam on 7 March 2014. 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 and course slides

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 after each course, so, please consult this page regularly.

First Period

• Lesson 1: 20 September 2013, by Antoine Miné.
  • introduction and course plan;
  • mathematical tools.
• Lesson 2: 27 September 2013, by Antoine Miné.
  • approximations;
  • program semantics (up to "finite traces semantics").
• Lesson 3: 4 October 2013, by Antoine Miné.
  • continuing on program semantics (from "infinite trace semantics" to the end),
  • program properties;
  • non-relational numeric abstract domains (up to "selected applications").
• Lesson 4: 11 October 2013, by Antoine Miné.
  • continuing on non-relational numeric abstract domains (from "generalities and notations" to the end).
• Lesson 5: 18 October 2013, by Antoine Miné.
  • relational numeric abstract domains;
  • abstracting non-linear programs.
• Lesson 6: 25 October 2013, by Jérôme Feret.
  • static analysis of digital filters;
  • arithmetic-geometric progression abstract domain.
• No course on 1 November 2013.
• Lesson 7: 8 November 2013, by Laurent Mauborgne.
  • symbolic abstract domains.
• Lesson 8: 15 November 2013, by Antoine Miné.
  • static analysis of concurrent programs.
• No course on 22 November 2013.
• No course on 29 November 2013.

Written exam: on 6 December 2013. (see also the former written exams)

• exam
• correction
• the grades are available on-line on the MPRI server

Second Period

• Lesson 9: 13 December 2013, by Xavier Rival.
  • semantics of programs and semantic properties.
• Lesson 10: 20 December 2013, by Xavier Rival.
  • partitioning abstractions.
• Lesson 11: 10 January 2014, by Jérôme Feret.
  • abstract interpretation of mobile systems.
• Lesson 12: 17 January 2014, by Jérôme Feret.
  • continuing on abstract interpretation of mobile systems.
• No course on 24 January 2014.
• Lesson 13: 31 January 2014, by Jérôme Feret.
  • abstract interpretation of protein-protein interactions networks.
• Lesson 14: 7 February 2014, by Jérôme Feret.
  • continuing on abstract interpretation of protein-protein interactions networks.
• Lesson 15: 14 February 2014, by Xavier Rival.
• Lesson 16: 21 February 2014, by Xavier Rival.
• No course on 28 February 2014.

Oral exam: on 7 March 2014.

Bibliography

There are no course notes for this course. In addition to perusing the course slides which are put on-line after each course, the students are encouraged to look at the following articles:

• P. Cousot. Verification by Abstract Interpretation. In International Symposium on Verification (Theory & Practice) celebrating Zohar Manna's $1000000_2$-th birthday, volume 2472 of LNCS, Springer, 2003.
• J. Bertrane, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, X. Rival. Static analysis and verification of aerospace software by abstract interpretation. In Proc. of AIAA Infotech@Aerospace (I@A 2010), number AIAA-2010-3385, 38 pages, Apr. 2010.

Former written exams

• Last year's exam.
• Former exams (and corrections) on Patrick Cousot's page.

Internship proposals

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.

• Compilation optimisante et certifiée pour la précision numérique, David Delmas et Matthieu Martel, équipe-projet DALI, laboratoire LIRMM, Université de Perpignan.
• Inferring sufficient numeric conditions with under-approximations by abstract interpretation, Antoine Miné, Équipe Abstraction, Département d'informatique, École normale supérieure.
• Static analysis by abstract interpretation of concurrent programs in weakly consistent memories, Antoine Miné, Équipe Abstraction, Département d'informatique, École normale supérieure.

---

Contact: