MPRI M2-6 Course, year 2020-2021

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

Mid-term exam

The subject for the mid-term exam is available here: partiel.pdf.

Please send back your answers by email before midnight on Monday 30 November to: antoine.mine at lip6.fr and xavier.rival at ens.fr.

Organization

The course takes place on Friday, from 12:45 to 15:45, at University Paris 7, Sophie Germain Building, room 1013.

The course is organized in two periods of 8 courses each.

The first period will begin on 18 September 2020. The first period will end with a 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 and course material

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 introductory articles and course notes for the first part of the course.

The 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 propose a project (in French). It is completely optional and not evaluated by the teachers.

First Period

• Lesson 1: 18 September 2020, 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.
  
  
  
• Lesson 2: 25 September 2020, by Antoine Miné.

  Topics: Semantics and properties.

  Slides:

  • 02: Program semantics and properties.

  Assignments:

  • Exercise (easy): prove the alternate characterization of Galois connection on slide 51 in the order theory slides.
  • Exercise: Part II of the 2014-2015 exam (Moore families); see the correction.
  
  
  
• Lesson 3: 2 October 2020, by Antoine Miné.

  Topics: Non-relational numeric abstract domains.

  Slides: 03: non-relational numeric domains.

  Assignments:

  • Exercises on trace abstraction, and the correction.
  • 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.
  • Additional exercises on the interval domain and the correction.
  
  
  
• Lesson 4: 9 October 2020, by Antoine Miné.

  Topics: Relational numeric abstract domains.

  Slides: 04: relational numeric domains.

  Assignments:

  • Exercise: Part III of the 2014-2015 exam (non-monotonicity of widening); see also the correction.
  • 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.

  A recording of the session (low quality, taken live) is available for registered students (contact us if you did not receive the link).
  
  

• Lesson 5: 23 October 2020, by Xavier Rival.

  Topics: Partitioning abstract domains.

  This lesson will be given online at the usual time (12:45 - 15:45) using Gotomeeting. Registered students have been sent a Gotomeeting link by email (contact us if you did not receive the link).

  Slides:

  • plain version
  • version with on-screen annotations taken during the class

  A recording of the session is also available for registered students at the same location as for last course's video (contact us if you did not receive the link).
  
  

• Lesson 6: 30 October 2020, by Caterina Urban.

  Topics: Abstract interpretation for liveness properties.

  Slides: 06: Abstract interpretation for liveness properties.

  This lesson will be virtual.

  Videos for the course are provided, and students are expected to watch the videos and read the slides in advance. We planned a Zoom meeting at the end of the slot (15:05 - 15:45) to answer all questions. Registered students should have received the link for the video and the Zoom meeting (contact us if you did not receive the link).
  
  

• Lesson 7: 13 November 2020, by Jérôme Feret.

  Topics: Qualitative abstraction of signaling pathways.

  This lesson will be given online at the usual time (12:45 - 15:45) using Gotomeeting. Registered students have been sent a Gotomeeting link by email (contact us if you did not receive the link).

  Slides:

  • 07a: Introduction
  • 07b: Reachability analysis of rule-based models
  
  
  
• Lesson 8: 20 November 2020, by Jérôme Feret.

  Topics: Abstraction of signaling pathways.

  This lesson will be given online at the usual time (12:45 - 15:45) using Gotomeeting. Registered students have been sent a Gotomeeting link by email (contact us if you did not receive the link).

  Slides:

  • 08a: Some notions of information flow.
  • 08b: Reduction of models of intra-cellular signalling pathways.

Mid-term exam: The mid-term exam will take place Monday 30 November at home.

• The exam will be available on this web page on Monday 30 November at 8 AM.
• You will have to send your answers by email before midnight.
• Possible formats to send your answers are: word-processor document, PDF document, or (clear, high-resolution) pictures or scan of (legible) hand-written sheets.
• You don't need to be online between the time you fetch the exam subject and the time you send your answer email.
• The format and length of the exam will be similar to the mid-term exams from the previous years.

Second Period

• Lesson 9: 11 December 2020, by Jérôme Feret.

  Topics: Specific numerical domains.

  This lesson will be given online at the usual time (12:45 - 15:45) using Gotomeeting. Registered students have been sent a Gotomeeting link by email (contact us if you did not receive the link).

  Slides:

  • 08a: Static analysis of digital filters.
  • 08b: The arithmetic-geometric progression abstract domain.
  
  
  
• Lesson 10: 18 December 2020, by Caterina Urban.

  Topics: Static analysis of neural networks.

  Slides: 10: Static analysis of neural networks.

  Reading assignments:

  • Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, Suman Jana: Efficient Formal Safety Analysis of Neural Networks. NeurIPS 2018: 6369-6379.
  • Hoang-Dung Tran, Diego Manzanas Lopez, Patrick Musau, Xiaodong Yang, Luan Viet Nguyen, Weiming Xiang, Taylor T. Johnson: Star-Based Reachability Analysis of Deep Neural Networks. FM 2019: 670-686.

  This lesson will be virtual.

  Videos for the course are provided, and students are expected to watch the videos and read the slides before the course. The optional reading assignments can be read after watching the course. We planned a Zoom meeting at the end of the slot (15:05 - 15:45) to answer all questions. Registered students should have received the link for the video and the Zoom meeting (contact us if you did not receive the link).
  
  

• Lesson 11: 8 January 2021, by Jérôme Feret.
• Lesson 12: 15 January 2021, by Jérôme Feret.

  Topics: Static analysis of mobile systems.

  These lessons will be given online at the usual time (12:45 - 15:45) using Gotomeeting. Registered students have been sent a Gotomeeting link by email (contact us if you did not receive the link).

  Slides: 11-12: Abstract interpretation mobile systems.
  
  

• Lesson 13: 22 January 2021, by Xavier Rival.

  Topics: Memory abstraction.

  This lesson will be given online at the usual time (12:45 - 15:45) using Gotomeeting. Registered students have been sent a Gotomeeting link by email (contact us if you did not receive the link).

  Slides:

  • plain version
  • version with on-screen annotations taken during the class
  
  
  
• Lesson 14: 29 January 2021, by Xavier Rival.

  Topics: Shape analysis abstractions.

  This lesson will be given online at the usual time (12:45 - 15:45) using Gotomeeting. Registered students have been sent a Gotomeeting link by email (contact us if you did not receive the link).

  Slides:

  • plain version
  • version with on-screen annotations taken during the class
  
  
  
• Lesson 15: 12 February 2021, by Xavier Rival.

  Topics: Analysis of security properties.

  This lesson will be given online at the usual time (12:45 - 15:45) using Gotomeeting. Registered students have been sent a Gotomeeting link by email (contact us if you did not receive the link).

  Slides:

  • plain version
  • version with on-screen annotations taken during the class
  
  
  
• Lesson 16: 19 February 2021, by Antoine Miné.

  Topics: Thread-modular static analysis of concurrent programs.

  This lesson will be given online at the usual time (12:45 - 15:45) using Zoom. Registered students have been sent a Zoom link by email (contact us if you did not receive the link).

  Slides:

  • 16: Thread-modular static analysis of concurrent programs..

Oral exam: date to be announced.

Reading material

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.

Course notes are available for the beginning of the course. They cover mainly lessons 1 to 4.

The contents of the later lessons is generally covered in articles. Each course will thus provide a specific bibliography in the course slides, for reference (reading is them 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 here 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.

---

Contact: