Generating Inductive Predicates for Symbolic Execution of Pointer-Manipulating Programs
Generating Inductive Predicates for Symbolic Execution of Pointer-Manipulating Programs
复制标题
为指针操作程序的符号执行生成归纳谓词
DOI：
10.1007/978-3-319-09108-2_5
复制
发表时间：
2014
影响因子：
3.7
通讯作者：
T. Noll
中科院分区：
文献类型：
--
作者：
Christina Jansen;Florian Göbe;T. Noll
研究了指针程序的两种抽象方法分离逻辑和超边替换文法之间的关系。两者都分别采用归纳定义的谓词和替换规则来表示（动态）数据结构，涉及符号执行的抽象和具体化操作。在分离逻辑的情况下，自动生成一个完整的操作集需要谓词的某些属性，这些属性目前是隐式描述和手动建立的。相反，保证语法抽象正确性的结构属性是可判定的和可自动化的。使用属性保持翻译，我们认为，正是这些属性的逻辑对应物，确保谓词定义的符号执行的直接适用性。
We study the relationship between two abstraction approaches for pointer programs, Separation Logic and hyperedge replacement grammars. Both employ inductively defined predicates and replacement rules, respectively, for representing (dynamic) data structures, involving abstraction and concretisation operations for symbolic execution. In the Separation Logic case, automatically generating a complete set of such operations requires certain properties of predicates, which are currently implicitly described and manually established. In contrast, the structural properties that guarantee correctness of grammar abstraction are decidable and automatable. Using a property-preserving translation we argue that it is exactly the logic counterparts of those properties that ensure the direct applicability of predicate definitions for symbolic execution.