MPRI M2-6 Course, year 2016-2017

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.

Organization

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

The course is organized in two periods of 8 courses each. The first period will begin on the 14 September 2016. 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: 14 September 2016, 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 (medium): Part II of the 2014-2015 exam (Moore families); see the correction.
Lesson 2: 21 September 2016, 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.
- Exercise: complete the proof on slide 33 (sufficient preconditions and reachability).
- Additional exercises on trace abstraction, and the correction (updated on 28/09/2016).
Lesson 3: 28 September 2016, by Antoine Miné.
Topics: Non-relational numerical abstract domains.
Slides: 03: non-relational numerical domains.
Assignments:
- Read slides 76 to 88 from lesson 2 (program semantics) about relational semantics.
- 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 (updated on 04/10/2016).
Lesson 4: 5 October 2016, by Antoine Miné.
Topics: Relational numerical abstract domains.
Slides: 04: relational numerical domains.
Assignments:
- Exercise (medium): 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: 12 October 2016, by Xavier Rival.
Topics: Partitioning abstractions.
Slides: 05: partitioning abstractions.
Assignments:
- Article reading: Abstract interpretation by dynamic partitioning. François Bourdoncle. JFP. 1990.
Lesson 6: 19 October 2016, by Xavier Rival.
Topics: Basic memory and shape abstractions.
Slides: 06: memory abstraction 1.
Assignments:
- Article reading: Parametric shape analysis via 3-valued logic. Mooly Sagiv, Thomas Reps, Reinhard Whilhelm. POPL 1999.
Lesson 7: 26 October 2016, by Xavier Rival.
Topics: Separation logic based shape abstraction.
Slides: 07: shape analysis based on separation logic.
Lesson 8: 02 November 2016, by Xavier Rival.
Topics: Program transformations as abstract interpretation
Slides: 08: program transformations as abstract interpretation.
Assignments:
- Prove the theorem at slide 79.
- Read: Systematic design of program transformation frameworks by abstract interpretation. Patrick Cousot, Radhia Cousot. POPL 2002: 178-190.

Written exam: on 30 November 2016.
(see also the former written exams)

Second Period

Lesson 9: 7 December 2016, by Antoine Miné.
Topics: Numeric analysis of concurrent programs.
Slides: 09: static analysis of concurrent programs.
Lesson 10: 14 December 2016, by Jérôme Feret.
Topics: Qualitative abstraction of signaling pathways.
Slides: 10: abstract interpretation of protein-protein interactions networks.
Lesson 11: 4 January 2017, by Jérôme Feret.
Topics: Quantitative abstractions of signaling pathways.
Slides: 11: abstract interpretation of protein-protein interactions networks.
No course on 11 January 2017.
Course is cancelled and moved to February.
Lesson 12: 18 January 2017, by Cezara Drăgoi.
Lesson 13: 25 January 2017, by Jérôme Feret.
Topics: Domain specific numerical domains.
Slides: 13a: The arithmetic-geometric progression abstract domain, 13b: static analysis of digital filters.
Lesson 14: 1 February 2017, by Jérôme Feret.
Topics: Static analysis of mobile systems I.
Slides: 14-15: abstract interpretation of mobile systems.
Lesson 15: 8 February 2017, by Jérôme Feret.
Topics: Static analysis of mobile systems II.
Slides: follow-up on last week's slides.
Lesson 16: 15 February 2017, by Cezara Drăgoi.

Oral exam: on 1st March 2017.

Bibliography

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

There is currently no reference book for the course.

Former written exams

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.

Contraintes sur des domaines paramétriques, Charlotte Truchet et David Cachera, Université de Nantes.
Separation Logic with Summary Predicates Described by Set Universal Quantification, Xavier Rival, École normale supérieure.
Separation Logic-based Abstraction, Three Valued Logic Abstraction and Reduction, Xavier Rival, École normale supérieure.
Static Analysis by Abstract Interpretation of Core Python Programs, Antoine Miné, LIP6, UPMC (Paris 6).

Contact: