Portal de Periódicos da CAPES

Generating Inductive Predicates for Symbolic Execution of Pointer-Manipulating Programs

2014; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-3-319-09108-2_5

1611-3349

Christina Jansen, Florian Göbe, Thomas Noll,

Software Engineering Research

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.