Polynomial Invariant Generation for Floating-Point Programs

TL;DR

This paper introduces a novel polynomial constraint solving framework for generating tight invariants in floating-point programs, effectively accounting for round-off errors to improve correctness verification.

Contribution

It presents the first polynomial constraint solving approach that explicitly handles floating-point round-off errors, combining error analysis with invariant generation.

Findings

Outperforms state-of-the-art methods in efficiency and precision

Successfully handles complex floating-point benchmarks

Reduces the computational cost of error variable management

Abstract

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.