浮点数到实区间算术的近似转换
Approximate Translation from Floating-Point to Real-Interval Arithmetic
摘要：
浮点运算（FPA）是实数运算（RA）的一种机械表示，其中每个运算都用舍入的对应运算代替。通过使用支持FPA逻辑的SMT解算器可以验证各种数值属性。然而，与RA相比，求解过程的可扩展性仍然有限。在本文中，我们提出了一个决定程序FPA，利用RA解决的效率。该方法将FP数抽象为有理区间，将FPA表达式抽象为区间算术（IA）表达式;然后，使用现成的RA求解器（我们使用CVC 4和Z3）求解IA公式以检查FPA公式的可满足性。为了换取抽象所获得的效率，求解过程变得准完整;当可满足性受到可能的数值错误的影响时，我们允许输出未知数。此外，我们的IA是精心形式化处理特殊值NaN。我们实现了所提出的方法，并在实验中将其与四个现有的SMT求解器进行了比较。因此，我们确认，我们的求解器是有效的舍入模式参数化的情况下。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
