Abstract Counterexample-Based Refinement for Powerset Domains
Abstract Counterexample-Based Refinement for Powerset Domains
复制标题
基于反例的抽象幂集域细化
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
Shmuel Sagiv
中科院分区：
文献类型：
--
作者：
R. Manevich;J. Field;T. Henzinger;G. Ramalingam;Shmuel Sagiv
反例引导的抽象精化（CEGAR）是一种强大的技术，可以将自动程序分析技术扩展到大型程序。然而，到目前为止，它主要用于模型检查的上下文中的谓词抽象。如果一个虚假的抽象反例需要通过抽象细化来移除，通常有几个选择，比如要细化哪个程序位置，在不同的位置使用哪个抽象域，以及要计算哪些抽象值。我们定义了几个合理的偏好排序抽象细化，如细化尽可能“晚”，尽可能“粗糙”。我们提出了通用的算法，找到最佳的细化相对于不同的偏好orderings.We还比较了不同的排序相对于所需的属性，包括属性，如果局部最优的细化组成的全局最优。最后，我们指出了一些困难与CEGAR的非幂集域。
Counterexample-guided abstraction refinement (CEGAR) is a powerful technique to scale automatic program analysis techniques to large programs. However, so far it has been used primarily formodel checking in the context of predicate abstraction.We formalize CEGAR for general powerset domains. If a spurious abstract counterexample needs to be removed through abstraction refinement, there are often several choices, such as which program location(s) to refine, which abstract domain(s) to use at different locations, and which abstract values to compute. We define several plausible preference orderings on abstraction refinements, such as refining as "late" as possible and as "coarse" as possible. We present generic algorithms for finding refinements that are optimal with respect to the different preference orderings.We also compare the different orderings with respect to desirable properties, including the property if locally optimal refinements compose to a global optimum. Finally, we point out some difficulties with CEGAR for non-powerset domains.