A Practical Approach to Interval Refinement for math.h/cmath Functions

TL;DR

This paper presents a practical interval refinement method for math.h/cmath functions in C++, enabling formal verification despite the lack of guarantees in standard libraries by exploiting their near-monotonicity and small glitches.

Contribution

It introduces novel interval refinement algorithms that handle non-correctly rounded functions, facilitating verification techniques like symbolic execution and abstract interpretation.

Findings

Effective detection of anomalous behaviors in real-world code

Ability to verify functions with small, rare glitches

First algorithms to handle non-correctly rounded implementations

Abstract

Verification of C++ programs has seen considerable progress in several areas, but not for programs that use these languages' mathematical libraries. The reason is that all libraries in widespread use come with no guarantees about the computed results. This would seem to prevent any attempt at formal verification of programs that use them: without a specification for the functions, no conclusion can be drawn statically about the behavior of the program. We propose an alternative to surrender. We introduce a pragmatic approach that leverages the fact that most math.h/cmath functions are almost piecewise monotonic: as we discovered through exhaustive testing, they may have glitches, often of very small size and in small numbers. We develop interval refinement techniques for such functions based on a modified dichotomic search, that enable verification via symbolic execution based model checking, abstract interpretation, and test data generation. Our refinement algorithms are the first in the literature to be able to handle non-correctly rounded function implementations, enabling verification in the presence of the most common implementations. We experimentally evaluate our approach on real-world code, showing its ability to detect or rule out anomalous behaviors.