Exploring Approximations for Floating-Point Arithmetic using UppSAT

TL;DR

This paper introduces UppSAT, a flexible framework for exploring and refining approximations in floating-point arithmetic constraints, aiding software verification with customizable encodings and decision procedures.

Contribution

UppSAT provides a systematic, extensible platform for experimenting with floating-point approximations in SMT solving, integrating multiple encodings and strategies.

Findings

UppSAT effectively combines various encodings for floating-point approximation.

Experimental results highlight trade-offs among different approximation strategies.

UppSAT facilitates flexible exploration of approximation refinements in floating-point verification.

Abstract

We consider the problem of solving floating-point constraints obtained from software verification. We present UppSAT --- a new implementation of a systematic approximation refinement framework [ZWR17] as an abstract SMT solver. Provided with an approximation and a decision procedure (implemented in an off-the-shelf SMT solver), UppSAT yields an approximating SMT solver. Additionally, UppSAT includes a library of predefined approximation components which can be combined and extended to define new encodings, orderings and solving strategies. We propose that UppSAT can be used as a sandbox for easy and flexible exploration of new approximations. To substantiate this, we explore several approximations of floating-point arithmetic. Approximations can be viewed as a composition of an encoding into a target theory, a precision ordering, and a number of strategies for model reconstruction and precision (or approximation) refinement. We present encodings of floating-point arithmetic into reduced precision floating-point arithmetic, real-arithmetic, and fixed-point arithmetic (encoded in the theory of bit-vectors). In an experimental evaluation, we compare the advantages and disadvantages of approximating solvers obtained by combining various encodings and decision procedures (based on existing state-of-the-art SMT solvers for floating-point, real, and bit-vector arithmetic).