Taming the Hydra: Targeted Control-Flow Transformations for Dynamic Symbolic Execution
Dynamic Symbolic Execution (DSE) suffers from the path explosion problem when the target program has many conditional branches. The classical approach for managing the path explosion problem is dynamic state merging. Dynamic state merging combines similar symbolic program states to avoid the exponential growth in the number of states during DSE. However, state merging still requires solver invocations at each program branch, even when both paths of the branch are feasible. Moreover, the best path search strategy for DSE may not create the best state merging opportunities. Some drawbacks of state merging can be mitigated by compile-time state merging (i.e., branch elimination by converting control-flow into dataflow). In this paper, we propose a non-semantics-preserving but failure-preserving compiler transformation for removing expensive symbolic branches in a program to improve the scalability of DSE. We have developed a framework for detecting spurious bugs that our transformation can insert. Finally, we show that our transformation can significantly improve the performance of DSE on various benchmark programs and help improve the performance of coverage and bug discovery of large real-world programs.
Mon 5 OctDisplayed time zone: Pacific Time (US & Canada) change
15:30 - 17:00 | |||
15:30 18mTalk | Spatial and Temporal Decomposition for Faster Translation Validation OOPSLA Benjamin Mikek Georgia Institute of Technology, Chathur Bommineni Georgia Institute of Technology, Qirun Zhang Georgia Institute of Technology, Thomas Reps University of Wisconsin-Madison DOI | ||
15:48 18mTalk | Efficient Extraction for Effectful E-graphs OOPSLA Oliver Flatt University of Washington, Anjali Pal University of Washington, Yihong Zhang University of Washington, Ryan Tjoa Jane Street, Kirsten Graham University of Washington, Alex Fischman University of Washington, Chandrakana Nandi Certora; University of Washington, Eli Rosenthal Google, Zachary Tatlock University of Washington, Haobin Ni University of Washington DOI | ||
16:06 18mTalk | Phaedrus: Predicting Dynamic Application Behavior with Lightweight Generative Models and LLMs OOPSLA Bodhisatwa Chatterjee NVIDIA, Georgia Institute of Technology, Neeraj Jadhav Georgia Institute of Technology, Santosh Pande Georgia Institute of Technology DOI | ||
16:24 18mTalk | Taming the Hydra: Targeted Control-Flow Transformations for Dynamic Symbolic Execution OOPSLA Charitha Saumya Intel, Muhammad Hassan Virginia Tech, Rohan Gangaraju University of Texas at Austin, Milind Kulkarni Purdue University, Kirshanthan Sundararajah Virginia Tech DOI Authorizer link Pre-print | ||