An Efficient Floating-Point Bit-Blasting API for Verifying C Programs
Abstract
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.
Cite
@article{arxiv.2004.12699,
title = {An Efficient Floating-Point Bit-Blasting API for Verifying C Programs},
author = {Mikhail R. Gadelha and Lucas C. Cordeiro and Denis A. Nicole},
journal= {arXiv preprint arXiv:2004.12699},
year = {2020}
}
Comments
20 pages