TACO: Efficient SAT-Based Bounded Verification Using Symmetry Breaking and Tight Bounds
TACO: Efficient SAT-Based Bounded Verification Using Symmetry Breaking and Tight Bounds
复制标题
DOI：
10.1109/tse.2013.15
复制
发表时间：
2013-09-01
影响因子：
7.4
通讯作者：
Frias, Marcelo F.
中科院分区：
文献类型：
--
作者：
Galeotti, Juan P.;Rosner, Nicolas;Frias, Marcelo F.
基于sat的带注释代码的有界验证包括将代码与注释一起转换为命题公式，并使用sat求解器分析公式是否违反规范。如果发现违反，则显示显示失败的执行跟踪。涉及具有复杂不变量的链接数据结构的代码尤其难以使用这些技术进行分析。在本文中，我们介绍了注释代码的翻译（TACO），这是一个原型工具，它实现了一种新颖的、通用的、全自动的技术，用于基于sat的分析处理复杂关联数据结构的jml注释Java顺序程序。我们使用对称破坏谓词来进行代码分析，一方面，它通过忽略某些同构模型类来减小搜索空间的大小，另一方面，它允许Java字段的紧密边界的并行、自动计算。实验表明，与基于sat的非仪器分析相比，转换到命题公式所需的命题变量显著减少，从而提高了分析效率的数量级。我们展示了在某些情况下，我们的工具可以发现基于sat求解、模型检查或smt求解的最先进工具无法检测到的错误。
SAT-based bounded verification of annotated code consists of translating the code together with the annotations to a propositional formula, and analyzing the formula for specification violations using a SAT-solver. If a violation is found, an execution trace exposing the failure is exhibited. Code involving linked data structures with intricate invariants is particularly hard to analyze using these techniques. In this paper, we present Translation of Annotated COde (TACO), a prototype tool which implements a novel, general, and fully automated technique for the SAT-based analysis of JML-annotated Java sequential programs dealing with complex linked data structures. We instrument code analysis with a symmetry-breaking predicate which, on one hand, reduces the size of the search space by ignoring certain classes of isomorphic models and, on the other hand, allows for the parallel, automated computation of tight bounds for Java fields. Experiments show that the translations to propositional formulas require significantly less propositional variables, leading to an improvement of the efficiency of the analysis of orders of magnitude, compared to the noninstrumented SAT-based analysis. We show that in some cases our tool can uncover bugs that cannot be detected by state-of-the-art tools based on SAT-solving, model checking, or SMT-solving.