TracerX: Dynamic Symbolic Execution with Interpolation
This work provides a significant improvement in program verification for developers and testers by enhancing the ability to determine reachability of target program points.
This paper introduces TracerX, a new interpolation algorithm implemented on KLEE, to address the path explosion problem in Dynamic Symbolic Execution (DSE) for program verification. It demonstrates that TracerX achieves a new level of code penetration success, especially for difficult targets, despite the overhead of interpolant computation.
Dynamic Symbolic Execution (DSE) is an important method for the testing of programs. An important system on DSE is KLEE which inputs a C/C++ program annotated with symbolic variables, compiles it into LLVM, and then emulates the execution paths of LLVM using a specified backtracking strategy. The major challenge in symbolic execution is path explosion. The method of abstraction learning has been used to address this. The key step here is the computation of an interpolant to represent the learnt abstraction. In this paper, we present a new interpolation algorithm and implement it on top of the KLEE system. The main objective is to address the path explosion problem in pursuit of code penetration: to prove that a target program point is either reachable or unreachable. That is, our focus is verification. We show that despite the overhead of computing interpolants, the pruning of the symbolic execution tree that interpolants provide often brings significant overall benefits. We then performed a comprehensive experimental evaluation against KLEE, as well as against one well-known system that is based on Static Symbolic Execution, CBMC. Our primary experiment shows code penetration success at a new level, particularly so when the target is hard to determine. A secondary experiment shows that our implementation is competitive for testing.