In numeric-intensive computations, it is well known that the execution of floating-point programs is imprecise as floating-point arithmetic incurs round-off errors. Although round-off errors are small for a single floating-point operation, the aggregation of such errors may be dramatic and cause catastrophic program failures. Therefore, to ensure the correctness of floating-point programs, round-off error needs to be carefully taken into account. In this work, we consider polynomial invariant generation for floating-point programs, aiming at generating tight invariants under the perturbation of round-off errors. Our contribution is a novel framework for applying polynomial constraint solving to address the invariant generation problem, which is also the first polynomial constraint solving based approach that handles floating-point errors to our best knowledge. In our framework, we propose a novel combination of round-off error analysis and polynomial constraint solving, aiming to circumvent the cost of handling a large number of error variables in the floating-point model. Experimental results over a variety of challenging benchmarks show that our framework outperforms SOTA approaches in both time efficiency and the precision of generated invariants.

翻译：在数值密集型计算中，浮点程序执行时因浮点运算引入舍入误差导致的结果不精确已是共识。尽管单次浮点运算的舍入误差极小，但此类误差的累积效应可能十分显著，甚至引发灾难性程序故障。因此，为确保浮点程序的正确性，必须审慎考虑舍入误差的影响。本文针对浮点程序的多项式不变量生成问题展开研究，旨在舍入误差扰动下生成紧致不变量。我们的核心贡献在于提出一种融合多项式约束求解的创新框架以解决不变量生成问题，据我们所知，这也是首个基于多项式约束求解处理浮点误差的方法。在该框架中，我们创新性地将舍入误差分析与多项式约束求解相结合，旨在规避浮点模型中需处理大量误差变量带来的计算开销。在多个具有挑战性的基准测试上的实验结果表明，本框架在时间效率与生成不变量精度上均优于现有最优方法。