Abstract Compilation for Verification of Numerical Accuracy Properties

TL;DR

This paper introduces a comprehensive framework combining runtime verification, abstract interpretation, and instrumentation to verify numerical accuracy properties in industrial software efficiently and soundly.

Contribution

It extends existing tools with rational numbers, develops an abstract compiler, and creates an instrumentation library, integrating these for improved accuracy verification.

Findings

Efficient analysis of industrial programs' accuracy.

Sound verification using combined techniques.

Effective restriction to numerical scenarios.

Abstract

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.