Static analysis for detecting and avoiding floating-point run-time errors in logic programs

The aim of this thesis is to provide techniques for the abstraction of floating-point expressions into the polyhedra domain as well as into the finite powerset of polyhedra domain. Moreover, this thesis aims at presenting a forward and a backward analysis for the detection and inference of floating-point errors such as overflow and division by zero. These techniques are based on abstract interpretation, which is a theory for the sound approximation of the semantics of programs. These abstractions and analyses have important applications for instance in engineering, mechanics and computer aided graphics design.

The abstraction of floating-point expressions into polyhedra includes two stages. the first, we present an approximation of floating-point expression by a polynomial with interval coefficients that includes the possible floating-point errors. In the second stage we present techniques for abstracting polynomials with interval coefficients into polyhedra and polyhedra powersets. Moreover, we present a technique for abstracting expressions in which a division by zero may occur.

A forward analysis for the detection of overflow and division by zero is then presented. This analysis is particular in that it always reaches the output of a programs. This an important requirement since the backward analysis needs information on the output to infer which input to a program could cause an overflow or a division by zero. Such analyses are important especially in the design of systems with high contents of nonlinear floating-point expressions. Experimental results show the usability of these analyses.