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.

翻译：在数值密集型计算中，众所周知浮点程序的执行存在不精确性，因为浮点运算会产生舍入误差。尽管单个浮点运算的舍入误差很小，但这些误差的累积可能非常显著，甚至导致灾难性的程序故障。因此，为了确保浮点程序的正确性，必须仔细考虑舍入误差。本文研究浮点程序的多项式不变式生成问题，旨在产生受舍入误差扰动下仍保持紧致的不变式。我们的贡献是一个应用多项式约束求解解决不变式生成问题的新框架，且据我们所知，这是首个基于多项式约束求解处理浮点误差的方法。在该框架中，我们提出了一种舍入误差分析与多项式约束求解的创新组合，旨在规避处理浮点模型中大量误差变量的计算成本。在多个具有挑战性的基准测试上的实验结果表明，我们的框架在时间效率和生成不变式的精度方面均优于现有最优方法。