  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.
