Approximate Translation from Floating-Point to Real-Interval Arithmetic

TL;DR

This paper introduces a decision procedure that abstracts floating-point arithmetic as interval arithmetic to leverage real arithmetic solvers, improving scalability while managing potential numerical errors.

Contribution

It presents a novel method that translates floating-point problems into interval arithmetic, enabling more efficient satisfiability checking with existing real arithmetic solvers.

Findings

The proposed solver is more efficient for parameterized rounding mode instances.

It handles NaN values meticulously in the interval arithmetic formalization.

Experimental results show improved performance over four existing SMT solvers.

Abstract

Floating-point arithmetic (FPA) is a mechanical representation of real arithmetic (RA), where each operation is replaced with a rounded counterpart. Various numerical properties can be verified by using SMT solvers that support the logic of FPA. However, the scalability of the solving process remains limited when compared to RA. In this paper, we present a decision procedure for FPA that takes advantage of the efficiency of RA solving. The proposed method abstracts FP numbers as rational intervals and FPA expressions as interval arithmetic (IA) expressions; then, we solve IA formulas to check the satisfiability of an FPA formula using an off-the-shelf RA solver (we use CVC4 and Z3). In exchange for the efficiency gained by abstraction, the solving process becomes quasi-complete; we allow to output unknown when the satisfiability is affected by possible numerical errors. Furthermore, our IA is meticulously formalized to handle the special value NaN. We implemented the proposed method and compared it to four existing SMT solvers in the experiments. As a result, we confirmed that our solver was efficient for instances where rounding modes were parameterized.