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 Jul Times are displayed in time zone: Tijuana, Baja California change
12:10 - 13:10
|Fast Bit-Vector Satisfiability|
Peisen YaoHKUST, Qingkai ShiThe Hong Kong University of Science and Technology, Heqing Huang, Charles ZhangThe Hong Kong University of Science and TechnologyDOI
|Relocatable Addressing Model for Symbolic Execution|
Technical PapersDOI Pre-print Media Attached
|Running Symbolic Execution Forever|
Frank BusseImperial College London, Martin NowackImperial College London, Cristian CadarImperial College LondonDOI Pre-print Media Attached