Type and Interval Aware Array Constraint Solving for Symbolic ExecutionACM SIGSOFT Distinguished Paper
Fri 16 Jul 2021 02:40 - 03:00 at ISSTA 2 - Session 14 (time band 2) Symbolic Execution 2 Chair(s): Martin Nowack
Array constraints are prevalent in analyzing a program with symbolic execution. Solving array constraints is challenging due to the complexity of the precise encoding for arrays. In this work, we propose to synergize symbolic execution and array constraint solving. Our method addresses the difficulties in solving array constraints with novel ideas. First, we propose a lightweight method for pre-checking the unsatisfiability of array constraints based on integer linear programming. Second, observing that encoding arrays at the byte-level introduces many redundant axioms that reduce the effectiveness of constraint solving, we propose type and interval aware axiom generation. Note that the type information of array variables is inferred by symbolic execution, whereas interval information is calculated through the above pre-checking step. We have implemented our methods based on KLEE and its underlying constraint solver STP and conducted large-scale experiments on 75 real-world programs. The experimental results show that our method effectively improves the efficiency of symbolic execution. Our method solves 182.56% more constraints and explores 277.56% more paths on average under the same time threshold.
Thu 15 JulDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
09:10 - 10:50 | Session 10 (time band 3) Symbolic Execution 1Technical Papers at ISSTA 2 Chair(s): Sébastien Bardin CEA LIST, University Paris-Saclay | ||
09:10 20mTalk | Fuzzing SMT Solvers via Two-Dimensional Input Space Exploration Technical Papers Peisen Yao Hong Kong University of Science and Technology, Heqing Huang Hong Kong University of Science and Technology, Wensheng Tang Hong Kong University of Science and Technology, Qingkai Shi Purdue University, Rongxin Wu Xiamen University, Charles Zhang Hong Kong University of Science and Technology DOI | ||
09:30 20mTalk | Boosting Symbolic Execution via Constraint Solving Time Prediction (Experience Paper) Technical Papers Sicheng Luo Fudan University, Hui Xu Fudan University, Yanxiang Bi Fudan University, Xin Wang Fudan University, Yangfan Zhou Fudan University DOI File Attached | ||
09:50 20mTalk | Synthesize Solving Strategy for Symbolic Execution Technical Papers Zhenbang Chen National University of Defense Technology, Zehua Chen National University of Defense Technology, Ziqi Shuai National University of Defense Technology, Guofeng Zhang Hunan University, Weiyu Pan National University of Defense Technology, Yufeng Zhang Hunan University, Ji Wang National University of Defense Technology DOI | ||
10:10 20mTalk | Type and Interval Aware Array Constraint Solving for Symbolic ExecutionACM SIGSOFT Distinguished Paper Technical Papers Ziqi Shuai National University of Defense Technology, Zhenbang Chen National University of Defense Technology, Yufeng Zhang Hunan University, Jun Sun Singapore Management University, Ji Wang National University of Defense Technology DOI | ||
10:30 20mTalk | Grammar-Agnostic Symbolic Execution by Token Symbolization Technical Papers Weiyu Pan National University of Defense Technology, Zhenbang Chen National University of Defense Technology, Guofeng Zhang Hunan University, Yunlai Luo National University of Defense Technology, Yufeng Zhang Hunan University, Ji Wang National University of Defense Technology DOI | ||
Fri 16 JulDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
02:00 - 03:20 | Session 14 (time band 2) Symbolic Execution 2Technical Papers at ISSTA 2 Chair(s): Martin Nowack Imperial College London | ||
02:00 20mTalk | Fuzzing SMT Solvers via Two-Dimensional Input Space Exploration Technical Papers Peisen Yao Hong Kong University of Science and Technology, Heqing Huang Hong Kong University of Science and Technology, Wensheng Tang Hong Kong University of Science and Technology, Qingkai Shi Purdue University, Rongxin Wu Xiamen University, Charles Zhang Hong Kong University of Science and Technology DOI | ||
02:20 20mTalk | Synthesize Solving Strategy for Symbolic Execution Technical Papers Zhenbang Chen National University of Defense Technology, Zehua Chen National University of Defense Technology, Ziqi Shuai National University of Defense Technology, Guofeng Zhang Hunan University, Weiyu Pan National University of Defense Technology, Yufeng Zhang Hunan University, Ji Wang National University of Defense Technology DOI | ||
02:40 20mTalk | Type and Interval Aware Array Constraint Solving for Symbolic ExecutionACM SIGSOFT Distinguished Paper Technical Papers Ziqi Shuai National University of Defense Technology, Zhenbang Chen National University of Defense Technology, Yufeng Zhang Hunan University, Jun Sun Singapore Management University, Ji Wang National University of Defense Technology DOI | ||
03:00 20mTalk | Grammar-Agnostic Symbolic Execution by Token Symbolization Technical Papers Weiyu Pan National University of Defense Technology, Zhenbang Chen National University of Defense Technology, Guofeng Zhang Hunan University, Yunlai Luo National University of Defense Technology, Yufeng Zhang Hunan University, Ji Wang National University of Defense Technology DOI | ||