MPRI M2-6 Course, year 2019-2020

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

Lesson 1: 11 September 2019, by Antoine Miné.
Topics: Course organization; Introduction; Order theory.
Slides:
- 00: introduction.
- 01: 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: 18 September 2019, by Antoine Miné.
Topics: Semantics and properties.
Slides: 02: program semantics (updated on 25/09/2019).
Assignments:
- Exercise: complete the proof on slide 38 (sufficient preconditions and reachability).
- Exercises on trace abstraction, and the correction.
- Exercise: Part I of the 2013-2014 exam (upper closure operators); see the correction.
- Read: M. Clarkson and F. Schneider. Hyperproperties. In Proc. of the 21st IEEE Computer Security Foundations Symposium, pp. 51-65, IEEE, 2008.
Lesson 3: 25 Septembre 2019, 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: 2 October 2019, 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 visiting the Apron library on GitHub.
Lesson 5: 16 October 2019, by Jérôme Feret.
Topics: Qualitative abstraction of signaling pathways.
Slides:
- 05a: Motivation.
- 05b: Reachability analysis of rule-based models.
Assignments:
- Prove the theorems on slide 32 and slide 43.
Lesson 6: 23 October 2019, by Jérôme Feret.
Topics: Abstraction of signaling pathways.
Slides:
Lesson 7: 30 October 2019, by Xavier Rival.
Topics: Memory abstractions.
Slides:
- 07: Memory abstraction I.
Lesson 8: 6 November 2019, by Jérôme Feret.
Topics: Specific numerical domain.
Slides:
- 08a: The arithmetic-geometric progression abstract domain.
- 08b: Static analysis of digital filters.
Assignments: exercices.

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

Second Period

Lesson 9: 4 December 2019, by Cezara Drăgoi.
Topics: Analysis of concurrent and distributed data structures.
Lesson 10: 11 December 2019, by Xavier Rival.
Topics: Partitioning abstractions.
Slides: 10: Partitioning abstractions.
Lesson 11: 18 December 2019, by Xavier Rival.
Topics: Memory abstractions.
Slides: 11: Shape analysis abstractions.
Lesson 12: 8 January 2020, by Jérôme Feret.
Lesson 13: 15 January 2020, by Jérôme Feret.
Topics: Static analysis of mobile systems.
Slides: 12: Abstract interpretation of mobile systems.
Assignment: Exercices.
~~Lesson 14: 29 January 2020, Antoine Miné.~~ Course cancelled.
Topics: Thread-modular static analysis of concurrent programs.
Lesson 15: 5 February 2020, by Xavier Rival.
Topics: Analysis of security properties.
Slides: Analysis of security properties.
Assignments: See last slide.
Lesson 16: 12 February 2020, by Cezara Drăgoi.
Topics: Analysis of concurrent and distributed data structures.

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:

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

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

2017-2018 exam (correction included).
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

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.

Algorithmic Fairness Static Analysis for Neural Networks, Caterina Urban (École Normale Supérieure & INRIA).
A General Framework for Input Data Usage Static Analysis, Caterina Urban (École Normale Supérieure & INRIA).
Abstract Domain Reduction Operation Beween Separation Logic Memory Abstraction And Value Abstraction, Xavier Rival (École Normale Supérieure & INRIA).

Contact: