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.
Wednesday mornings, 9h-12h15, Salle de cours 1168 then salle TD 1106 (R. Franklin), Turing LIX/INRIA Building 1st floor, Ecole Polytechnique:
Evaluation will be based on the following (monomes or binomes accepted, naturally more work will be expected from binomes) :