MPRI M2-6 Course, year 2014-2015

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 1009 en 2014, and room 2027 starting on the 7 January 2015 (access map, local copy).

The course is organized in two periods of 8 courses each. The first period will begin on the 17 September 2014. The first period will end with a 3-hour written exam on the 3 December 2014 (usual room and hours). 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: 17 September 2014, by Antoine Miné.

  Topics: Course organization; Introduction; Order theory.

  Slides: 00: organisation, 01: introduction, 02: order theory (updated on 24/09/2014).

  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 48 in the order theory slides.
  • Exercise (hard): try solving Part I of last year's exam (upper closure operators); see the correction.
  
  
  
• Lesson 2: 24 September 2014, by Antoine Miné.

  Topics: State and traces semantics; State and trace properties.

  Slides: 03: program semantics (updated on 24/09/2014).

  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 39 (sufficient preconditions and reachability).
  • Additional exercises on trace abstraction (updated on 30/09/2014) and correction.
  
  
  
• Lesson 3: 1 October 2014, by Antoine Miné.

  Topics: Non-relational numerical abstract domains.

  Slides: 04: non-relational numerical domains (updated on 01/10/2014).

  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.
  • Exercises on the interval domain (updated on 07/10/2014) and correction.
  
  
  
• Lesson 4: 8 October 2014, by Antoine Miné.

  Topics: Relational numerical abstract domains.

  Slides: 05: relational numerical domains (updated on 08/10/2014).

  Assignments:

  • 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: 15 October 2014, by Caterina Urban and Antoine Miné.

  Topics: Inferring ranking functions for termination; Non-linear and floating-point abstractions.

  Slides: 06: non-linear and floating-point abstractions (updated on 15/10/2014), 07: automatic inference of ranking functions by abstract interpretation.

  Assignments:

  • Practical exercise: Experiment with the online academic termination analyzer.
  • Exercise: Part II of last year's exam (template abstract domain); see the correction.
  
  
  
• No lesson on the 22 October 2014.
  
  
• Lesson 6: 29 October 2014, by Xavier Rival.

  Topics: Partitioning abstractions.

  Slides: 08: partitioning abstractions

  Assignments:

  • Read F. Bourdoncle Abstract interpretation by dynamic partitioning. Journal of Functional Programming, 2(4) 407–423, 1992.
  • Exercise: formalize the transfer functions for the trace partitioning domain where partitioning is guided by a loop (slide 82).
  
  
  
• Lesson 7: 5 November 2014, by Jérôme Feret.

  Topics: Domain-specific numerical abstract domains.

  Slides: 09: static analysis of digital filters, 10: the arithmetic-geometric progression abstract domain.

  Assignments:

  • Read J.Feret The Arithmetic-Geometric Progression Abstract Domain. In Verification, Model Checking and Abstract Interpretation, LNCS 3385. 2005, Springer.
  • Read J.Feret Static Analysis of Digital Filters. In European Symposium on Programming, LNCS 2986. 2004, Springer.
  • Exercices.
  
  
  
• Lesson 8: 12 November 2014, by Antoine Miné.

  Topics: Analysis of Concurrent Programs.

  Slides: 11: static analysis of concurrent programs (updated on 13/11/2014).

  No assignment: to prepare for the written exam, review the previous assignments and the former written exams.
  
  

• No lesson on the 19 November 2014.
  

Written exam: on 3 December 2014. (see also the former written exams)

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

Second Period

• Lesson 9: 10 December 2014, by Xavier Rival.

  Topics: Abstraction of memory states.

  Slides: 12: Memory Abstraction 1.

  Assignments:

  • Exercise: Formalize the transfer functions for the null pointer analysis at slide 64 (easy).
  • Read: Alain Deutch. Interprocedural May-Alias Analysis for Pointers: Beyond k-limiting. In Proc. PLDI 1994: 230-241.
  
  
  
• Lesson 10: 17 December 2014, by Xavier Rival (room 1009).

  Topics: Shape analysis based on separation logic.

  Slides: 13: Shape analysis based on separation logic.

  Assignments:

  • Read: John C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In Proc. LICS 2002: 22-25.
  
  
  
• Lesson 11: 7 January 2015, by Jérôme Feret (room 2027).

  Topics: Static analysis of mobile systems (semantics).

  Slides: 14: Abstract Interpretation of Mobile Systems.

  Assignments:

  • Exercises.
  
  
  
• Lesson 12: 14 January 2015, by Jérôme Feret (room 2027).

  Topics: Static analysis of mobile systems (abstraction).

  Slides: 15: Abstract Interpretation of Mobile Systems.

  Assignments:

  • Read: M. Karr. Affine relationships among variables of a program. In Acta Informatica 14.V.1976, Volume 6, Issue 2, pp 133-151.
  
  
  
• Lesson 13: 21 January 2015, by Xavier Rival (room 2027).

  Topics: Program transformations as abstract interpretations.

  Slides: 16: Program transformation as abstract interpretation.

  Assignments:

  • Exercice: Formalize the dead variable elimination correctness (slide 46)
  • Read: P. Cousot and R. Cousot. Systematic design of program transformation frameworks by abstract interpretation. In Conference Record of the 29th Symposium on Principles of Programming Languages (POPL’02), pages 178–190, Portland, Oregon, January 2002.
  
  
  
• No lesson on the 28 January 2015.
  
  
• Lesson 14: 4 February 2015, by Laurent Mauborgne (room 2027).

  Topics: The Astrée static analyzer: Abstract Interpretation in practice.

  Slides: Astreé: Abstract interpretation in practice
  
  

• Lesson 15: 11 February 2015, by Jérôme Feret (room 2027).

  Topics: Static analysis of biological systems (qualitative abstractions).

  Slides: Abstract interpretation of protein-protein interactions networks.

  Assignments:

  • Exercise: prove Theorem 1 (slide 27) and Theorem 3 (slide 34).
  
  
  
• Lesson 16: 18 February 2015, by Jérôme Feret (room 2027).

  Topics: Static analysis of biological systems (quantitative abstractions).

  Slides: Slides.

No lesson on the 25 February 2015.

Oral exam: on 11 March 2015.

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 Proc. of AIAA Infotech@Aerospace (I@A 2010), number AIAA-2010-3385, 38 pages, Apr. 2010.

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

• Last year's 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.

• Static analysis by abstract interpretation of the functional correctness of vector and matrix manipulating programs, Antoine Miné, Équipe Abstraction, Département d'informatique, École normale supérieure.
• Accurate and Efficient Disjunctions of Abstract Properties of Memory States, Xavier Rival, Équipe Abstraction, Département d'informatique, École normale supérieure.
• Abstraction de Relations entre États de la Mémoire, Xavier Rival, Équipe Abstraction, Département d'informatique, École normale supérieure.
• A weaklky relational domain to detect potential polymerisation events in signaling pathways, Jérôme Feret, Équipe Abstraction, Département d'informatique, École normale supérieure.
• Approximate model reduction for the differential semantics of rule-based models, Jérôme Feret, Équipe Abstraction, Département d'informatique, École normale supérieure.

---

Contact: