Static Analysis
Static Analysis
复制标题
静态分析
DOI：
10.1007/978-3-642-38856-9_22
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Brain M
中科院分区：
文献类型：
--
作者：
Brain M
求解器提高效率的一种方法是将推理委托给抽象领域。使用抽象域的求解器不支持插值，并且不能用于基于插值的验证。我们扩展抽象冲突驱动的子句学习（acdcl）求解器与证明生成和插值。我们的研究结果导致第一插值过程的浮点逻辑，随后，第一插值为基础的验证程序与浮点变量。我们证明了这种方法的潜力，通过验证一些程序，这是目前的验证工具的挑战。
One approach forsmtsolvers to improve efficiency is to delegate reasoning to abstract domains. Solvers using abstract domains do not support interpolation and cannot be used for interpolation-based verification. We extend Abstract Conflict Driven Clause Learning (acdcl) solvers with proof generation and interpolation. Our results lead to the first interpolation procedure for floating-point logic and subsequently, the first interpolation-based verifiers for programs with floating-point variables. We demonstrate the potential of this approach by verifying a number of programs which are challenging for current verification tools.