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.
Mon 20 JulDisplayed time zone: Tijuana, Baja California change
12:10 - 13:10
|Fast Bit-Vector Satisfiability|
Peisen Yao HKUST, Qingkai Shi The Hong Kong University of Science and Technology, Heqing Huang , Charles Zhang The Hong Kong University of Science and TechnologyDOI
|Relocatable Addressing Model for Symbolic Execution|
Technical PapersDOI Pre-print Media Attached
|Running Symbolic Execution Forever|
Frank Busse Imperial College London, Martin Nowack Imperial College London, Cristian Cadar Imperial College LondonDOI Pre-print Media Attached