Partial Solution Based Constraint Solving Cache in Symbolic Execution
Constraint solving is one of the main challenges for symbolic execution. Caching is an effective mechanism to reduce the number of the solver invocations in symbolic execution and is adopted by many mainstream symbolic execution engines. However, caching can not perform well on all programs. How to improve caching’s effectiveness is challenging in general. In this work, we propose a partial solution-based caching method for improving caching’s effectiveness. Our key idea is to utilize the partial solutions inside the constraint solving to generate more cache entries. A partial solution may satisfy other constraints of symbolic execution. Hence, our partial solution-based caching method naturally improves the rate of cache hits. We have implemented our method on two mainstream symbolic executors (KLEE and Symbolic PathFinder) and two SMT solvers (STP and Z3). The results of extensive experiments on real-world benchmarks demonstrate that our method effectively increases the number of the explored paths in symbolic execution. Our caching method achieves 1.07x to 2.3x speedups for exploring the same amount of paths on different benchmarks.
Fri 19 JulDisplayed time zone: Brasilia, Distrito Federal, Brazil change
11:00 - 12:30 | Testing 4Research Papers / Industry Papers at Pitanga Chair(s): Antonia Bertolino National Research Council, Italy | ||
11:00 18mTalk | Partial Solution Based Constraint Solving Cache in Symbolic Execution Research Papers Ziqi Shuai School of Computer, National University of Defense Technology, China, Zhenbang Chen College of Computer, National University of Defense Technology, Kelin Ma School of Computer, National University of Defense Technology, China, Kunlin Liu School of Computer, National University of Defense Technology, China, Yufeng Zhang Hunan University, Jun Sun School of Information Systems, Singapore Management University, Singapore, Ji Wang School of Computer, National University of Defense Technology, China Pre-print | ||
11:18 18mTalk | Natural Symbolic Execution-based Testing for Big Data Analytics Research Papers Yaoxuan Wu UCLA, Ahmad Humayun Virginia Tech, Muhammad Ali Gulzar Virginia Tech, Miryung Kim UCLA and Amazon Web Services Pre-print | ||
11:36 18mTalk | MTAS: A Reference-Free Approach for Evaluating Abstractive Summarization Systems Research Papers Xiaoyan Zhu Zhejiang Sci-Tech University, Mingyue Jiang Zhejiang Sci-Tech University, Xiao-Yi Zhang University of Science and Technology Beijing, Liming Nie Nanyang Technological University, Zuohua Ding Zhejiang Sci-Tech University | ||
11:54 18mTalk | Observation-based unit test generation at Meta Industry Papers Mark Harman Meta Platforms, Inc. and UCL, Rotem Tal Meta platforms, Alexandru Marginean Meta platforms, Eddy Wang Meta platforms, Nadia Alshahwan Meta Platforms | ||
12:12 18mTalk | Property-based Testing for Validating User Privacy-Related Functionalities in Social Media Apps Industry Papers Jingling Sun University of Electronic Science and Technology of China, Ting Su East China Normal University, Jun Sun School of Information Systems, Singapore Management University, Singapore, Jianwen Li East China Normal University, China, Mengfei Wang ByteDance, Geguang Pu East China Normal University, China | ||