验证C程序的高效浮点位爆破API（CS LO）---Elva

我们描述了一种新的用于浮点的SMT位爆破API，并在几个C程序的验证过程中使用不同的SMT解算器对其进行了评估。新的浮点API是ESBMC中SMT后端的一部分，它是一种最先进的C和C++的有界模型检验器。为了进行评估，我们将我们的浮点API与Z3和MathSAT中的本机浮点API进行了比较，结果表明，Boolector在使用浮点API时，比使用本机浮点API的解算器性能更好，能够在更短的时间内正确地验证更多的程序。实验结果还表明，我们在ESBMC中实现的浮点API与其他最先进的软件验证程序是相当的。此外，当使用浮点运算验证程序时，我们的新浮点API没有产生错误的答案。

原文题目：An Efficient Floating-Point Bit-Blasting API for Verifying C Programs

原文：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.

原文作者：Mikhail R. Gadelha, Lucas C. Cordeiro, Denis A. Nicole

原文链接：https://arxiv.org/abs/2004.12699