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.
symbolic execution memory model abstract symbol table static analysis
Dai Ziying Mao Xiaoguang Ma Xiaodong Wang Rui
School of Computer, National University of Defense Technology (NUDT), Changsha 410073, China
国际会议
重庆
英文
20-24
2009-12-25（万方平台首次上网日期，不代表论文的发表时间）