Sound static analysis of run-time errors in programs with floating-point computations

12/10/2015
Speaker(s) : Antoine Miné (APR, UPMC)
 Static analysis consists in automatically inferring properties of the set of executions of a program at compile-time, without executing it. To scale up to large programs, analyzers employ approximations. A sound analysis will however always err on the safe side and consider a super-set of program executions. The success of tools such as Astrée has shown that sound static analysis is able to certify important properties, such as the absence of run-time errors in industrial embedded C programs.
Floating-point computations are difficult to handle soundly due to pervasive rounding. This is particularly the case when inferring relations between variables, as relational analyses rely heavily on algebraic identities of real numbers that no longer hold in float. In this talk, we will discuss some solutions and address two problems: how to soundly analyze programs that feature floating-point computations, and how to implement a sound relational static analyzer that itself uses floating-point computations. We will discuss the application of the methods to the detection of run-time errors.