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.

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