Precise software analysis and verification require tracking the exact path along which a statement is executed (path-sensitivity), the different contexts from which a function is called (context-sensitivity), and the bit-accurate operations performed. Previously, verification with such precision has been considered too inefficient to scale to large software. In this paper, we present a novel approach to solving such verification conditions, based on an automatic abstraction-checking-refinement framework that exploits natural abstraction boundaries present in software. Experimental results show that our approach easily scales to over 200,000 lines of real C/C++ code.
展开▼
机译：精确的软件分析和验证需要跟踪执行语句的确切路径（路径敏感度），调用函数所处的不同上下文（上下文敏感度）以及执行的位精确操作。以前，这种精度的验证被认为效率太低，无法扩展到大型软件。在本文中，我们提出了一种基于自动抽象检查优化框架的解决此类验证条件的新颖方法，该框架利用了软件中存在的自然抽象边界。实验结果表明，我们的方法可以轻松扩展到超过200,000行的实际C / C ++代码。
展开▼
