用于验证C程序的高效浮点位级展开API
计算机科学中的逻辑
2020-04-30 v2 软件工程
摘要
我们描述了一个新的用于浮点数的SMT位级展开（bit-blasting）API，并在验证若干C程序时使用不同的现成SMT求解器对其进行了评估。该新浮点API是ESBMC（一种最先进的C/C++有界模型检测器）中SMT后端的一部分。在评估中，我们将我们的浮点API与Z3和MathSAT中的原生浮点API进行了比较。我们表明，Boolector在使用该浮点API时优于具有原生浮点支持的求解器，能在更短时间内正确验证更多程序。实验结果还表明，我们在ESBMC中实现的浮点API与其他最先进的软件验证器相当。此外，在验证带有浮点运算的程序时，我们的新浮点API未产生任何错误答案。
引用
@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}
}
备注
20 pages