Write a Blog >>
ISSTA 2021
Sun 11 - Sat 17 July 2021 Online
co-located with ECOOP and ISSTA 2021
Thu 15 Jul 2021 09:10 - 09:30 at ISSTA 2 - Session 10 (time band 3) Symbolic Execution 1 Chair(s): S├ębastien Bardin
Fri 16 Jul 2021 02:00 - 02:20 at ISSTA 2 - Session 14 (time band 2) Symbolic Execution 2 Chair(s): Martin Nowack

Satisfiability Modulo Theories (SMT) solvers serve as the core engine of many techniques, such as symbolic execution. Therefore, ensuring the robustness and correctness of SMT solvers is critical. While fuzzing is an efficient and effective method for validating the quality of SMT solvers, we observe that prior fuzzing work only focused on generating various first-order formulas as the inputs but neglected the algorithmic configuration space of an SMT solver, which leads to under-reporting many deeply-hidden bugs. In this paper, we present Falcon, a fuzzing technique that explores both the formula space and the configuration space. Combining the two spaces significantly enlarges the search space and makes it challenging to detect bugs efficiently. We solve this problem by utilizing the correlations between the two spaces to reduce the search space, and introducing an adaptive mutation strategy to boost the search efficiency. During six months of extensive testing, Falcon finds 518 confirmed bugs in CVC4 and Z3, two state-of-the-art SMT solvers, 469 of which have already been fixed. Compared to two state-of-the-art fuzzers, Falcon detects 38 and 44 more bugs and improves the coverage by a large margin in 24 hours of testing.

Thu 15 Jul

Displayed 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
20m
Talk
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
20m
Talk
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
20m
Talk
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
20m
Talk
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
20m
Talk
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 Jul

Displayed 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
20m
Talk
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
20m
Talk
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
20m
Talk
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
20m
Talk
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