MPRI M2-6 Course, year 2017-2018

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 on the M2-6 page on the MPRI site.

Organization

The course takes place on Wednesday, from 8:45 to 11:45, at University Paris 7, Sophie Germain Building, room 2035.

The course is organized in two periods of 8 courses each. The first period will begin on the 13 September 2017. 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 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.

First Period

Lesson 1: 13 September 2017, by Antoine Miné.
Topics: Course organization; Introduction; Order theory.
Slides: 01a: organisation, 01b: introduction, 01c: order theory.
Assignments:
- Read: P. Cousot. Abstract Interpretation Based Formal Methods and Future Challenges. In Informatics, 10 Years Back - 10 Years Ahead, LNCS 2000, pp. 138-156, Springer, 2001.
- Exercise (easy): prove the alternate characterization of Galois connection on slide 49 in the order theory slides.
- Exercise: Part II of the 2014-2015 exam (Moore families); see the correction.
Lesson 2: 20 September 2017, by Antoine Miné.
Topics: State and traces semantics; State and trace properties.
Slides: 02: program semantics.
Assignments:
- Read: M. Clarkson and F. Schneider. Hyperproperties. In Proc. of the 21st IEEE Computer Security Foundations Symposium, pp. 51-65, IEEE, 2008.
- Exercises on trace abstraction, and the correction.
- Exercise: Part I of the 2013-2014 exam (upper closure operators); see the correction.
Lesson 3: 27 September 2017, by Antoine Miné.
Topics: Non-relational numeric abstract domains.
Slides: 03: non-relational numeric domains.
Assignments:
- Read: N. Halbwachs and J. Henry. When the decreasing sequence fails. In Proc. of the 19th International Static Analysis Symposium, pp. 198-213, LNCS 7460, Springer, 2012.
- Exercise: Part III of the 2014-2015 exam (non-monotonicity of widening); see also the correction.
- Additional exercises on the interval domain and the correction.
Lesson 4: 4 October 2017, by Antoine Miné.
Topics: Relational numeric abstract domains.
Slides: 04: relational numeric domains.
Assignments:
- Exercise: Part II of the 2013-2014 exam (Template abstract domain); see the correction.
- Practical exercice: Experiment with the on-line academic Interproc analyzer. Try the examples provided in the interface, some examples from the course, and propose your own examples. Different abstract domains are available: try them and compare them.
- Read: B. Jeannet and A. Miné. Apron: A library of numerical abstract domains for static analysis. In Proc. of the 21st International Conference on Computer Aided Verification (CAV 2009), pp. 661-667, LNCS 5643, Springer, 2009. This gives you some insight on how numeric abstract domains are implemented and used in real applications. You can complete this reading by going to the web-page of the Apron library and taking a look at the API documentation (both a C binding and an OCaml binding are available).
Lesson 5: 11 October 2017, by Xavier Rival.
Topics: Partitioning abstractions.
Slides: 05: Partitioning abstractions.
Assignments:
- Exercices and reading assignment on the last slide of the course.
Lesson 6: 18 October 2017, by Xavier Rival.
Topics: Basic memory and shape abstractions.
Slides: 06: Memory abstraction.
Assignments:
- Exercices and reading assignment on the last slide of the course.
Lesson 7: 25 October 2017, by Xavier Rival.
Topics: Separation logic based shape abstractions.
Slides: 07: Shape analysis based on separation logic.
Assignments:
- Exercices and reading assignment on the side 93 of the course.
Lesson 8: 8 November 2017, by Antoine Miné.
Topics: Numeric analysis of concurrent programs.
Slides: 08: static analysis of concurrent programs.

Written exam: on 29 November 2017.
(see also the former written exams)

Second Period

Lesson 9: 6 December 2017, by Cezara Drăgoi.
Topics: Static analysis for shared memory data structures.
Lesson 10: 13 December 2017, by Cezara Drăgoi.
Topics: Programming abstractions for static analysis of distributed data structures.
Lesson 11: 20 December 2017, by Jérôme Feret.
Slides: 11a: The arithmetic-geometric progression abstract domain, 11b: Static analysis of digital filters.
Lesson 12: 10 January 2018, by Jérôme Feret.
Slides: 12a: Abstract interpretation of protein-protein interactions networks, 12b: Reachability analysis of rule-based models.
Lesson 13: 17 January 2018, by Jérôme Feret.
Lesson 14: 24 January 2018, by Jérôme Feret.
Lesson 15: 31 January 2018, by Jérôme Feret.
Lesson 16: 7 February 2018, by Xavier Rival.
Topics: Program transformations as abstract interpretation
Slides: 16: Program transformations as abstract interpretation.

Oral exam: on 7 March 2018.

Course Notes, Bibliography

Preliminary course notes covering mainly lessons 1, 3, and 4 are available, per request, by email at .

The following articles give an taste of the contents and the goal of the course:

P. Cousot. Verification by Abstract Interpretation. In International Symposium on Verification (Theory & Practice) celebrating Zohar Manna's 1000000₂-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 Foundations and Trends in Programming Languages (FnTPL), 2(2–3), 71–190, 2015. Now Publishers.

Additionally, a course-specific bibliography is provided in the course slides (for reference; reading is not mandatory).

Former written exams

2016-2017 exam.
2015-2016 exam, and its correction.
2014-2015 exam, and its correction.
2013-2014 exam and its correction.
2012-2013 exam.
Exams from before 2012 (and corrections) are available 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.

Contact: