Boolean Heaps
Boolean Heaps
复制标题
布尔堆
DOI：
10.1007/11547662_19
复制
发表时间：
2005
影响因子：
8.7
通讯作者：
Thomas Wies
中科院分区：
文献类型：
--
作者：
A. Podelski;Thomas Wies
我们证明了在谓词抽象的框架中，可以对堆对象上的谓词进行强制转换。这导致了Sagiv， Reps和Wilhelm对三值形状分析的潜在概念的另一种观点。抽象post操作符的构造类似于经典谓词抽象的相应构造，不同之处在于，堆上对象的谓词取代了状态谓词，布尔堆（位向量集合）取代了布尔状态（位向量）。一个程序被抽象为一个布尔堆上的程序。对于程序的每个命令，通过演绎推理，即应用最弱前提算子和蕴涵检验，有效地构造出相应的抽象命令。因此，我们获得了形状分析的符号框架。
We show that the idea of predicates on heap objects can be cast in the framework of predicate abstraction. This leads to an alternative view on the underlying concepts of three-valued shape analysis by Sagiv, Reps and Wilhelm. Our construction of the abstract post operator is analogous to the corresponding construction for classical predicate abstraction, except that predicates over objects on the heap take the place of state predicates, and boolean heaps (sets of bitvectors) take the place of boolean states (bitvectors). A program is abstracted to a program over boolean heaps. For each command of the program, the corresponding abstract command is effectively constructed by deductive reasoning, namely by the application of the weakest precondition operator and an entailment test. We thus obtain a symbolic framework for shape analysis.