Abstract:

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 and syntax in the source codes. This paper addresses this problem by proposing a new concept of abstract symbol table and a method to model memory using abstract symbol tables. The abstract symbol table records names, types, abstract addresses and symbolic values of addressable objects, which is a simple and accurate memory abstracting mechanism. The memory model is prerequisite for any techniques involving symbolic execution, but this paper systematically presents a memory model for symbolic execution in detail. The abstract symbol tablebased memory model can handle various data types and syntax uniformly including function and class, handle the aliasing problem directly, and possess good scalability because of several performanceimproving techniques.

Key words: symbolic execution;memory model;abstract symbol table, program analysis