Up

Heap Cloning: Enabling Dynamic Symbolic Execution of Java Program

Heap Cloning: Enabling Dynamic Symbolic Execution of Java Program
1 · 2

dynamic symbolic execution Java JNI

Their previous paper is Type-Dependence Analysis and Program Transformation for Symbolic Execution.

1 To be able to compute PC, one should take in account language features. For Java there are native methods, reflection, etc. A quantitative evaluation of the contribution of native code to Java workloads sais, native methods in the SPEC JVM98 (read about this spec) ranges from 45 K to 5 M. They said, modifying JVM is one of the ways to perform DSE for Java. But, none of the existing SE (not DSE!) tools for Java are based on this approach: difficult to implement and maintain. They mean the JVM or any virtual machine? They said, one of the features of DSE: if you cannot execute something symbolically, you can execute in concretely. (You cannot do it in pure SE.) They links to Dart and CUTE.

2 They consider two approaches: JVM modification and code instrumentation. Their technique is heap cloning: transformation PP'. P' uses copies of the original classes and use “concrete heap” and “symbolic heap”.

Sergey Vartanov, 2007–2020