Relational Abstract Domains for the Detection of Floating-Point Run-Time Errors

TL;DR

This paper introduces a novel approach to adapt relational abstract domains for static analysis of floating-point computations, enabling detection of run-time errors like overflows and invalid operations in IEEE 754 floating-point arithmetic.

Contribution

It extends existing numerical abstract domains to handle floating-point non-linearity using linear forms with interval coefficients, improving static error detection capabilities.

Findings

Effective detection of floating-point run-time errors

Extension of octagon abstract domain for floating-point analysis

Experimental results demonstrate practical applicability

Abstract

We present a new idea to adapt relational abstract domains to the analysis of IEEE 754-compliant floating-point numbers in order to statically detect, through abstract Interpretation-based static analyses, potential floating-point run-time exceptions such as overflows or invalid operations. In order to take the non-linearity of rounding into account, expressions are modeled as linear forms with interval coefficients. We show how to extend already existing numerical abstract domains, such as the octagon abstract domain, to efficiently abstract transfer functions based on interval linear forms. We discuss specific fixpoint stabilization techniques and give some experimental results.