FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Exploring Approximations for Floating-Point Arithmetic using UppSAT

Authors: Peter Backeman, Aleksandar Zeljić, Christoph M. Wintersteiger and Philipp Rümmer

Paper Information

Title:Exploring Approximations for Floating-Point Arithmetic using UppSAT
Authors:Peter Backeman, Aleksandar Zeljić, Christoph M. Wintersteiger and Philipp Rümmer
Proceedings:IJCAR Proceedings 9th IJCAR, 2018
Editors: Stephan Schulz, Didier Galmiche and Roberto Sebastiani
Keywords:SAT, SMT, Approximation, Floating Point Arithmetic
Abstract:

ABSTRACT. We consider the problem of solving floating-point constraints obtained from software verification. We present UppSAT - an new implementation of a systematic approximation refinement framework 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 into the theory of bit-vectors in practice). 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).

Pages:16
Talk:Jul 15 11:00 (Session 103E: SMT 2)
Paper: