Symbolic Execution of Floating-point Programs: How far are we?
Floating-point programs are challenging for symbolic execution due to the constraint solving problem. To investigate the effectiveness and limitations of the existing methods, we conduct the first empirical study in this paper on five existing symbolic execution methods for floating-point programs. We have implemented the existing methods on the state-of-the-art symbolic execution KLEE and use the real-world representative floating-point programs as the benchmarks, which are used to evaluate the existing methods with respect to code coverage and bug finding. The results indicate that the existing methods complement each other in bug finding. Based on the findings of the experimental results, we propose synergizing the existing methods to improve symbolic execution’s effectiveness. The experimental results demonstrate our synergic method can detect more bugs.
Fri 9 DecDisplayed time zone: Osaka, Sapporo, Tokyo change
13:00 - 14:00 | |||
13:00 20mPaper | Symbolic Execution of Floating-point Programs: How far are we? Technical Track Guofeng Zhang National University of Defense Technology, Zhenbang Chen National University of Defense Technology, Ziqi Shuai National University of Defense Technology | ||
13:20 20mPaper | Optimal Refinement-based Array Constraint Solving for Symbolic Execution Technical Track Meixi Liu National University of Defense Technology, Changsha, China, Ziqi Shuai National University of Defense Technology, Luyao Liu National University of Defense Technology, Kelin Ma National University of Defense Technology, Ke Ma | ||
13:40 20mPaper | Synergizing Symbolic Execution and Fuzzing By Function-level Selective Symbolization Technical Track Guofeng Zhang National University of Defense Technology, Zhenbang Chen National University of Defense Technology, Ziqi Shuai National University of Defense Technology, Yufeng Zhang Hunan University, Ji Wang College of Computer, National University of Defense Technology |