论文标题
用于验证C程序的有效的浮点小束缚API
An Efficient Floating-Point Bit-Blasting API for Verifying C Programs
论文作者
论文摘要
我们描述了一种用于浮点的新的SMT爆炸API，并在验证多个C程序期间使用不同的现成的SMT求解器对其进行了评估。新的浮点API是ESBMC中SMT后端的一部分，ESBMC是C和C ++的最新有限模型检查器。为了进行评估，我们将浮点API与Z3和Mathsat中的本机浮点API进行了比较。我们表明，在使用浮点API时，Boolector以对浮点数的本机支持优于求解器，从而在更少的时间内正确验证更多程序。实验结果还表明，我们在ESBMC中实现的浮点API与其他最先进的软件验证器相当。此外，当使用浮点算术验证程序时，我们的新浮点API不会产生错误的答案。
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.
