An Efficient Floating-Point Bit-Blasting API for Verifying C Programs
This work addresses verification challenges for C/C++ programs with floating-point operations, offering an incremental improvement in efficiency and accuracy for software verifiers.
The authors tackled the problem of verifying C programs with floating-point arithmetic by developing a new SMT bit-blasting API, which outperformed native solvers like Z3 and MathSAT in correctly verifying more programs in less time and produced no wrong answers.
We describe a new SMT bit-blasting API for floating-points and evaluate it using different out-of-the-shelf SMT solvers during the verification of several C programs. The new floating-point API is part of the SMT backend in ESBMC, a state-of-the-art bounded model checker for C and C++. For the evaluation, we compared our floating-point API against the native floating-point APIs in Z3 and MathSAT. We show that Boolector, when using floating-point API, outperforms the solvers with native support for floating-points, correctly verifying more programs in less time. Experimental results also show that our floating-point API implemented in ESBMC is on par with other state-of-the-art software verifiers. Furthermore, when verifying programs with floating-point arithmetic, our new floating-point API produced no wrong answers.