Exploring Approximations for Floating-Point Arithmetic using UppSAT
Exploring Approximations for Floating-Point Arithmetic using UppSAT
复制标题
使用 UppSAT 探索浮点运算的近似值
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Philipp Rümmer
中科院分区：
文献类型：
--
作者：
Aleksandar Zeljić;Peter Backeman;C. Wintersteiger;Philipp Rümmer
我们考虑解决从软件验证获得的浮点约束的问题。我们将UPPSAT提出---作为一个抽象的SMT求解器的系统近似细化框架[ZWR17]的新实现。 Uppsat提供了一个近似值和决策程序（以现成的SMT求解器实现），可产生一个近似的SMT求解器。此外，UppSAT包括一个预定义近似组件的库，可以将其组合并扩展以定义新的编码，顺序和解决策略。我们建议将Uppsat用作沙箱，以便于对新近似值进行易于灵活探索。为了证实这一点，我们探讨了浮点算术的几个近似值。近似值可以看作是编码为目标理论的组成，精确排序以及模型重建和精度（或近似）改进的许多策略。我们将浮点算术的编码介绍为降低的精确浮点算术，实算术和固定点算术的编码（在比特矢量理论中编码）。在实验评估中，我们比较通过组合各种编码和决策程序（基于现有的最新SMT求解器，用于浮动点，真实和比特矢量算术）获得的近似求解器的优点和缺点。
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).
影响因子：
0.8
作者：
Brain, Martin;D'Silva, Vijay;Kroening, Daniel
通讯作者：
Kroening, Daniel
抽象冲突驱动学习
DOI：
10.1145/2429069.2429087
发表时间：
2013
期刊：
--
影响因子：
--
作者：
D'Silva V
通讯作者：
D'Silva V