Description

Instructor:
Sylvie Putot
Office: LIX - UMR 7161
1 rue Honoré d'Estienne d'Orves
Bâtiment Alan Turing, Campus X
Email: Sylvie.Putot@polytechnique.edu

This course explores theoretical foundations and practical tools for software verification, with a focus on abstract interpretation based static analysis. Using an abstraction of the program semantics allows us to automatically synthesize inductive program properties. Verification of safety-critical embedded programs is a natural field of application of such techniques. A difficulty that arises is the necessity to take into account the interaction of the program with its physical environment. The system of interest is then hybrid, coupling discrete and continuous components. The second part of the course is devoted to an introduction to the modeling and analysis of such systems.

Topics

  1. Program analysis (4 lectures)
    • Semantic equations, fixpoint computation
    • Abstract interpretation
    • Interval analysis
    • Relational and numerical abstract domains
  2. Introduction to hybrid systems verification (3 lectures)

Your feedback on the course

Poll on the course (feedback is important!)

Schedule

Wednesday mornings, 9h-12h10, exceptionally Monday afternoon on September 18, (Salle de cours 1169 + Salle TD 1101 (R. Franklin), Turing LIX/INRIA Building 1st floor, Ecole Polytechnique:

  • September 13,
  • September 18 (Monday!), 14h-17h00
  • September 20,
  • September 27,
  • October 4,
  • October 18,
  • November 8,
  • November 15, 9h-12h (oral defenses of final project, PC ?)

Evaluation of the course

Evaluation will be based on the following (monomes or binomes accepted, naturally more work will be expected from binomes) :

  • Lab sessions 1 to 4 (designing and experimenting an analysis with PAG) : send code and report by email (putot@lix.polytechnique.fr), strict deadline October 3
  • Project (starting October 4) : send code and report by email (strict deadline November 12) + oral defense on November 15