Trabalho em anais de eventoOpen Access
An Efficient Floating-Point Bit-Blasting API for Verifying C Programs
GADELHA, M. Y. R.; CORDEIRO, L. C.; NICOLE, D
Resumo
Resumo
. 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 floatingpoint API implemented in ESBMC is on par with other state-of-the-art software verifiers. Furthermore, when verifying programs with floatingpoint arithmetic, our new floating-point API produced no wrong answers.
palavras-chave
Palavras-chave
SMT solversC program verificationESBMCbounded model checkingfloating-point arithmeticZ3software verification
Status
Published
links
Links e arquivos
Trabalho em anais de evento