Static Analysis of Numerical Programs and Systems
Sylvie Putot, CEA-List & Ecole Polytechnique, Palaiseau, France.
Proving the software reliability of safety-critical embedded systems is a major challenge in our era, where numerical computing is becoming more and more important. In this course, we will present abstract interpretation based methods for the static analysis of numerical properties systems. I will begin with an introduction to abstract interpretation, a theory that makes it possible to automatically synthesize invariant properties on programs. I will then illustrate it with a family of abstract domains based on zonotopes, that are well suited to the analysis of numerical computations. I will in particular demonstrate how they can be adapted to bound the errors due to the use of finite precision to represent real numbers. I will finally end with some examples with the static analyzer Fluctuat.