Compositional Invariant Checking for Overlaid and Nested Linked Lists
Compositional Invariant Checking for Overlaid and Nested Linked Lists
复制标题
重叠和嵌套链接列表的组合不变检查
DOI：
10.1007/978-3-642-37036-6_9
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
M. Sighireanu
中科院分区：
文献类型：
--
作者：
C. Enea;Vlad Saveluc;M. Sighireanu
我们引入了一段分离逻辑，称为NOLL，用于对操作重叠和嵌套链表的程序进行自动推理，其中重叠意味着这些列表共享相同的对象集。NOLL的显著特征是：(1)它由一组指定嵌套链接列表段的用户定义的谓词来参数化，(2)允许共享对象位置但不记录字段位置的分离合取的“每字段”版本，以及(3)它可以表达列表段之间的共享约束。我们利用一个小的模型性质证明了检验两个NOLL公式之间的蕴涵是co-NP完全的。我们还提供了一种检查NOLL中蕴涵的有效方法，它首先构造两个公式的布尔抽象以推导出所有的隐式约束，然后检查这两个公式之间是否存在同态，并将其视为图。我们已经实现了这个过程，并将其应用于几个处理覆盖和嵌套数据结构的有趣案例研究生成的验证条件。
We introduce a fragment of separation logic, calledNOLL, for automated reasoning about programs manipulating overlaid and nested linked lists, where overlaid means that the lists share the same set of objects. The distinguishing features ofNOLLare: (1) it is parametrized by a set of user-defined predicates specifying nested linked list segments, (2) a “per-field” version of the separating conjunction allowing to share object locations but not record field locations, and (3) it can express sharing constraints between list segments. We prove that checking the entailment between twoNOLLformulas is co-NP complete using a small model property. We also provide an effective procedure for checking entailment inNOLL, which first constructs a Boolean abstraction of the two formulas in order to infer all the implicit constraints, and then, it checks the existence of a homomorphism between the two formulas, viewed as graphs. We have implemented this procedure and applied it on verification conditions generated from several interesting case studies that manipulate overlaid and nested data structures.