Abstract
Patrick Cousot, professor at the École Normale Supérieure, presented abstract interpretation, which he and his team have been developing for thirty years. The idea is to symbolically compute the program according to the same execution laws, but on more abstract data, such as intervals or polygons instead of individual numbers. This makes it possible to obtain a superior approximation of all possible calculations in finite time, and to detect the impossibility of certain critical errors: access to an array outside its bounds, division by zero, arithmetic overflow (the error that led to the explosion of Ariane 501).
Abstract interpretation is based on a mathematically sophisticated general framework and the development of a collection of abstract domains (intervals, octagons, ellipsoids, etc.). Its implementation requires subtle engineering to combine the properties of the different domains. It has been industrialized by several companies (Polyspace, AbsInt, etc.). P. Cousot's team has developed the Astrée software, used by Airbus to verify the absence of arithmetic exceptions in the A380's piloting code, making it one of the greatest successes of formal verification today.
