Abstract Compilation for Verification of Numerical Accuracy Properties
This work addresses the problem of numerical accuracy verification for industrial software, presenting an incremental combination of existing methods.
The paper tackles the challenge of verifying numerical accuracy in software by introducing a framework that combines runtime monitoring, abstract compilation, and instrumentation to analyze accuracy properties. Initial experiments indicate the technique can efficiently and soundly analyze industrial programs by focusing on specific numerical scenarios.
Verification of numerical accuracy properties in modern software remains an important and challenging task. This paper describes an original framework combining different solutions for numerical accuracy. First, we extend an existing runtime verification tool called E-ACSL with rational numbers to monitor accuracy properties at runtime. Second, we present an abstract compiler, FLDCompiler, that performs a source-to-source transformation such that the execution of the resulting program, called an abstract execution, is an abstract interpretation of the initial program. Third, we propose an instrumentation library FLDLib that formally propagates accuracy properties along an abstract execution. While each of these solutions has its own interest, we emphasize the benefits of their combination for an industrial setting. Initial experiments show that the proposed technique can efficiently and soundly analyze the accuracy of industrial programs by restricting the analysis on thin numerical scenarios.