GT Pequan
Sound static analysis of run-time errors in programs with floating-point computations
10/12/2015Intervenant(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.
Plus d'informations ici
marc (at)
nullmezzarobba.net
