Dynamic Path Pruning in Symbolic Execution

Ying Shen Chen, Wei Ning Chen, Che Yu Wu, Hsu Chun Hsiao, Shih-Kun Huang

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review


To alleviate path explosion in symbolic execution, path pruning removes unsatisfiable paths at an early stage before they multiply. Although existing symbolic execution platforms have implemented several path pruning strategies to determine whether and when to check a path's satisfiability, it remains unclear how effective these strategies are because the time to check a path's satisfiability is non-negligible and may vary drastically. This work proposes dynamic path pruning (DPP), a strategy that aims to minimize the overall exploration time by dynamically adjusting the path checking rate. DPP assigns a higher checking rate to paths that are more likely to be unsatisfiable, and the likelihood is estimated based on the observed program's characteristics, such as the observed percentage of satisfiable paths. DPP is implemented on top of an open source symbolic execution platform in only a few hundred lines. Our evaluation confirms that DPP consistently achieves near-optimal exploration time for a wide spectrum of programs, whereas existing static path pruning strategies suffer from unacceptable worst-case performance due to their program-independent behaviors. Compared with static strategies, DPP performs best in 84% (110 out of 131) of CGC binaries, and the exploration time is within 100-124% of the best static strategy in 95% of the tested handcrafted and coreutils binaries.

Original languageEnglish
Title of host publicationDSC 2018 - 2018 IEEE Conference on Dependable and Secure Computing
PublisherInstitute of Electrical and Electronics Engineers Inc.
ISBN (Electronic)9781538657904
StatePublished - 23 Jan 2019
Event2018 IEEE Conference on Dependable and Secure Computing, DSC 2018 - Kaohsiung, Taiwan
Duration: 10 Dec 201813 Dec 2018

Publication series

NameDSC 2018 - 2018 IEEE Conference on Dependable and Secure Computing


Conference2018 IEEE Conference on Dependable and Secure Computing, DSC 2018


Dive into the research topics of 'Dynamic Path Pruning in Symbolic Execution'. Together they form a unique fingerprint.

Cite this