Date Added: Sep 2011
The dynamic symbolic-execution technique can automatically perform symbolic execution of programs that use problematic features of Java, such as native methods. However, to compute precise symbolic execution, the technique requires manual effort to specify models for problematic code. Furthermore, existing approaches to perform symbolic execution either cannot be extended to perform dynamic symbolic execution or incur significant imprecision. In this paper, the authors present a novel program-transformation technique called heap cloning. Heap cloning transforms a program in such a way that dynamic symbolic execution of the transformed program results in the same path constraints as dynamic symbolic execution of the original program.