A Memory Model for Symbolic Execution

Symbolic execution plays an important role in the area of software testing and program verification. However, there are several difficulties facing symbolic execution, one of which is how to abstract various data types in source codes. This paper addresses this problem by proposing a memory model that is based on the abstract symbol table. The abstract symbol table records names, abstract addresses and symbolic values of variables, which is a simple and accurate memory abstracting mechanism. The memory model is prerequisite for any technique involving symbolic execution, but this paper is the first one that systematically presents a memory model for symbolic execution that can handle various data types uniformly. Moreover, pointer arithmetic is supported, and the aliasing problem can be handled implicitly, so no extra alias algorithm is needed.