MPRI M2-6 Course, year 2015-2016

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, local copy).

The course is organized in two periods of 8 courses each. The first period will begin on the 16 September 2015. 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: 16 September 2015, by Antoine Miné.

  Topics: Course organization; Introduction; Order theory.

  Slides: 00: organisation, 01: introduction, 02: 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 48 in the order theory slides.
  • Exercise (medium): Part II of the 2014-2015 exam (Moore families); see the correction.
  • Exercise (hard): Part I of the 2013-2014 exam (upper closure operators); see the correction.
  
  
  
• Lesson 2: 23 September 2015, by Antoine Miné.

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

  Slides: 03: program semantics (updated on 29/09/2015).

  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.
  
  
  
• Lesson 3: 30 Septembre 2015, by Antoine Miné.

  Topics: State and trace semantics (continued from last week).

  Slides: second part of last week's slides.
  
  
  
  

• No course on 7 October 2015.
  • Correction of lesson 3 exercises.
  
  
  
• Lesson 4: 14 October 2015, by Antoine Miné.

  Topics: Non-relational numerical abstract domains.

  Slides: 04: non-relational numerical domains (updated on 20/10/2015).

  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, see the correction (added on 20/10/2015).
  
  
  
• Lesson 5: 21 October 2015, by Antoine Miné.

  Topics: Relational numerical abstract domains.

  Slides: 05: relational numerical domains.

  Assignments:

  • Exercise (medium): Part III of the 2014-2015 exam (non-monotonicity of widening); 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 6: 28 October 2015, by Antoine Miné.

  Topics: Numeric analysis of concurrent programs.

  Slides: 06: static analysis of concurrent programs.
  
  

• Lesson 7: 4 Novembre 2015, by Jérôme Feret.

  Topics: Qualitative abstraction of signaling pathways.

  Slides: 07: abstract interpretation of protein-protein interactions networks.

  Assignments:

  • Exercise: prove the absence of false alarm, in slide 43 of the course.
  
  
  
• No course on 11 November 2015.
  
  
• Lesson 8: 18 Novembre 2015, by Jérôme Feret.

  Topics: Quantitative abstractions of signaling pathways.

  Slides: 08: reduction of models of intra-cellular signalling pathways.
  
  

Written exam: on 2 December 2015.
(see also the former written exams)

Second Period

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

  Topics: Domain specific numerical domains.

  Slides: Specific numerical domains.

  Assignments:

  • Exercices.
  
  
  
• Lesson 10: 16 December 2015, by Xavier Rival.

  Topics: Partitioning abstractions.

  Slides: Partitioning abstractions.
  
  

• Lesson 11: 6 January 2016, by Xavier Rival.

  Topics: Abstraction of memory states.

  Slides: Memory abstraction.
  
  

• Lesson 12: 13 January 2016, by Xavier Rival.

  Topics: Shape analysis based on separation logic.

  Slides: Shape analysis based on separation logic.
  
  

• No course on 20 January 2016.
  
  
• Lesson 13: 27 January 2016, by Xavier Rival.

  Topics: Program transformations as abstract interpretation.

  Slides: Program transformations as abstract interpretation.
  
  

• Lesson 14: 3 February 2016, by Jérôme Feret.

  Topics: Mobile systems.
  
  

• Lesson 15: 10 February 2016, by Jérôme Feret.

  Topics: Static analysis of mobile systems.
  
  

• No course on 17 February 2016. The course is moved to 24 February.
  
  
• Lesson 16: 24 February 2016, by Cezara Drăgoi.

  Topics: Static analysis for concurrent data structures.

Oral exam: on 8 March 2016.

The information for the oral exam has been sent by email. Please contact the teachers if you have not received an email.

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

• to be announced...

---

Contact: