堆抽象的逻辑特征
摘要：形状分析涉及确定在对动态分配的存储进行破坏性更新的程序中的“形状不变性”问题。在最近的研究中，我们展示了如何使用基于三值一阶逻辑的抽象解释来执行形状分析。在该工作中，具体存储是有限的二值逻辑结构，并且可以在执行期间可能出现的存储集合通过一种特定的有限的三值逻辑结构（保守地）表示。在本文中，我们展示了如何使用具有传递闭包的一阶逻辑公式来刻画在形状分析中出现的三值结构。我们还为三值一阶逻辑定义了非标准（“超值”）语义，比传统的三值语义更精确，并证明超值语义可以使用现有的定理证明器有效地实现。
作者：G. Yorsh, T. Reps, M. Sagiv, R. Wilhelm
论文ID：cs/0312014
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23