| Sl.No. | Presenter(s) | Title | Duration |
|---|---|---|---|
| 1 | Sangharatna Godboley National Institute of Technology | Warangal (nitw.ac.in) |
Tracer-X: Dynamic Symbolic Execution with Interpolation | Half day |
| Abstract: Dynamic Symbolic Execution (DSE) is an important method for 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 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. We show that despite the overhead of computing interpolants, the pruning of the symbolic execution tree that interpolants provide often significant overall benefits. We performed a comprehensive experimental evaluation against KLEE, as well as against two well-known systems that are based on Static Symbolic Execution (SSE), CBMC and LLBMC. Our primary conclusion is that we can perform complete search to a new level. A secondary conclusion is that when our search is incomplete, we are competitive or better than the baseline compared systems in terms of code coverage and bug finding. Half-day is required for this topic because, the basic concepts will take 1 hour and the advanced concepts with illustrative examples will take 2-3 hours. |
|||