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.

Conference Day
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 BardinCEA LIST, University Paris-Saclay
09:10
20m
Talk
Fuzzing SMT Solvers via Two-Dimensional Input Space Exploration
Technical Papers
Peisen YaoHong Kong University of Science and Technology, Heqing HuangHong Kong University of Science and Technology, Tang WenshengHong Kong University of Science and Technology, Qingkai ShiHong Kong University of Science and Technology, Rongxin WuXiamen University, Charles ZhangHong Kong University of Science and Technology
DOI
09:30
20m
Talk
Boosting Symbolic Execution via Constraint Solving Time Prediction (Experience Paper)
Technical Papers
Sicheng LuoFudan University, Hui XuFudan University, Yanxiang BiFudan University, Xin WangFudan University, Yangfan ZhouFudan University
DOI
09:50
20m
Talk
Synthesize Solving Strategy for Symbolic Execution
Technical Papers
Zhenbang ChenNational University of Defense Technology, Zehua ChenNational University of Defense Technology, Ziqi ShuaiNational University of Defense Technology, Guofeng ZhangHunan University, Weiyu PanNational University of Defense Technology, Yufeng ZhangHunan University, Ji WangNational 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 ShuaiNational University of Defense Technology, Zhenbang ChenNational University of Defense Technology, Yufeng ZhangHunan University, Jun SunSingapore Management University, Ji WangNational University of Defense Technology
DOI
10:30
20m
Talk
Grammar-Agnostic Symbolic Execution by Token Symbolization
Technical Papers
Weiyu PanNational University of Defense Technology, Zhenbang ChenNational University of Defense Technology, Guofeng ZhangHunan University, Yunlai LuoNational University of Defense Technology, Yufeng ZhangHunan University, Ji WangNational University of Defense Technology
DOI

Conference Day
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 NowackImperial College London
02:00
20m
Talk
Fuzzing SMT Solvers via Two-Dimensional Input Space Exploration
Technical Papers
Peisen YaoHong Kong University of Science and Technology, Heqing HuangHong Kong University of Science and Technology, Tang WenshengHong Kong University of Science and Technology, Qingkai ShiHong Kong University of Science and Technology, Rongxin WuXiamen University, Charles ZhangHong Kong University of Science and Technology
DOI
02:20
20m
Talk
Synthesize Solving Strategy for Symbolic Execution
Technical Papers
Zhenbang ChenNational University of Defense Technology, Zehua ChenNational University of Defense Technology, Ziqi ShuaiNational University of Defense Technology, Guofeng ZhangHunan University, Weiyu PanNational University of Defense Technology, Yufeng ZhangHunan University, Ji WangNational 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 ShuaiNational University of Defense Technology, Zhenbang ChenNational University of Defense Technology, Yufeng ZhangHunan University, Jun SunSingapore Management University, Ji WangNational University of Defense Technology
DOI
03:00
20m
Talk
Grammar-Agnostic Symbolic Execution by Token Symbolization
Technical Papers
Weiyu PanNational University of Defense Technology, Zhenbang ChenNational University of Defense Technology, Guofeng ZhangHunan University, Yunlai LuoNational University of Defense Technology, Yufeng ZhangHunan University, Ji WangNational University of Defense Technology
DOI