Abstract domain for floating-point programs

Abstract

Floating point numbers are widely used nowadays in programs but the verification of programs using this type of arithmetic is not trivial at all. This is due to the nature of floating-point arithmetic and the loss of precision when trying to represent real numbers in a computer. On the other hand, abstract interpretation has demonstrated to be effective in capturing different code behaviors and a number of different approaches have been proposed for analyzing floating point, numerical programs. Among these approaches, we decided to implement within the Ciao abstract interpretation framework and study a non-relational interval analysis capturing the behavior of constraints of type x = y · z. We extended this analysis to different representations of real numbers with the hope of providing a tool for the developer in order to choose the most suitable type when coding. The objective is to be able to minimize the consumption of memory while controlling the loss of precision, which unfortunately is unavoidable in this computations. With this domain we have been able to run some experiments with industrial code obtaining some encouraging results. We also propose a number of research lines stemming from several possible extensions this work.

Los números en coma flotante aparecen en prácticamente todos los programas actuales, sin embargo, verificarlos cuando se usa esta aritmética no es en absoluto trivial. Esto se debe a la naturaleza de la aritmética en coma flotante y a la pérdida de precisión provocada al tratar de representar números reales en un ordenador. Por otro lado, la interpretación abstracta ha demostrado ser una técnica efectiva a la hora de capturar diversos comportamientos del código. Se han propuesto numerosas aproximaciones a este problema usando las técnicas de interpretación abstracta y entre todas ellas hemos decidido estudiar e implementar dentro del Sistema Ciao un dominio no relacional basado en intervalos, el cual captura restricciones de la forma x = y · z. Hemos extendido este análisis para diferentes representaciones de los números reales utilizadas en la actualidad, con la esperanza de ayudar a los desarrolladores a escoger el tipo de dato numérico más apropiado a la hora de programar. Esto permitiría reducir el consumo de memoria mientras se mantiene bajo control la perdida de precisión, la cual desgraciadamente siempre va a existir. Con este dominio hemos sido capaces de analizar fragmentos de código industrial obteniendo resultados que nos animan a continuar por alguna de las múltiples líneas que puedan aparecer como extensión de este trabajo.