Running symbolic execution forever
Frank Busse, Martin Nowack, Cristian Cadar
Abstract
When symbolic execution is used to analyse real-world applications, it often consumes all available memory in a relatively short amount of time, sometimes making it impossible to analyse an application for an extended period. In this paper, we present a technique that can record an ongoing symbolic execution analysis to disk and selectively restore paths of interest later, making it possible to run symbolic execution indefinitely. To be successful, our approach addresses several essential research challenges related to detecting divergences on re-execution, storing long-running executions efficiently, changing search heuristics during re-execution, and providing a global view of the stored execution. Our extensive evaluation of 93 Linux applications shows that our approach is practical, enabling these applications to run for days while continuing to explore new execution paths. CCS CONCEPTS • Software and its engineering → Software testing and debugging.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext 1bdb33b0-a06d-401a-8c75-d95d972d3ce3Cited by top-tier papers5
- Learning to Explore Paths for Symbolic ExecutionJingxuan He, Gishor Sivanrupan, Petar Tsankov, Martin T. VechevCCS 2021 · 39 citations
- On the Feasibility of Automated Built-in Function Modeling for PHP Symbolic ExecutionPenghui Li, Wei Meng, Kangjie Lu, Changhua LuoWWW 2021 · 18 citations
- Combining Structured Static Code Information and Dynamic Symbolic Traces for Software Vulnerability PredictionHuanting Wang, Zhanyong Tang, Shin Hwei Tan, Jie Wang et al.ICSE 2024 · 15 citations
- Pending Constraints in Symbolic Execution for Better Exploration and SeedingTimotej Kapus, Frank Busse, Cristian CadarASE 2020 · 8 citations
- Empc: Effective Path Prioritization for Symbolic Execution with Path CoverShuangjie Yao, Dongdong SheS&P 2025
Related papers
- A bounded symbolic-size model for symbolic executionDavid Trabish, Shachar Itzhaky, Noam RinetzkyFSE 2021 · 10 citations
- Combining static analysis error traces with dynamic symbolic execution (experience paper)Frank Busse, Pritam M. Gharat, Cristian Cadar, Alastair F. DonaldsonISSTA 2022 · 11 citations
- Relocatable addressing model for symbolic executionDavid Trabish, Noam RinetzkyISSTA 2020 · 10 citations
- C^2SR: Cybercrime Scene Reconstruction for Post-mortem Forensic AnalysisYonghwi Kwon, Weihang Wang, Jinho Jung, Kyu Hyung Lee et al.NDSS 2021
- Natural Symbolic Execution-Based Testing for Big Data AnalyticsYaoxuan Wu, Ahmad Humayun, Muhammad Ali Gulzar, Miryung KimFSE 2024 · 5 citations
