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

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.


  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)


Wednesday mornings, 9h-12h15, Salle de cours 1168 then salle TD 1106 (R. Franklin), Turing LIX/INRIA Building 1st floor, Ecole Polytechnique:

  • September 12,
  • September 19,
  • October 3,
  • October 10,
  • October 17,
  • October 24,
  • November 7,
  • November 14, 9h-12h (oral defense of final project)

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 (, strict deadline October 16
  • Project (starting October 17) : send code and report by email (strict deadline November 11) + oral defense on November 14