Running symbolic execution forever
File(s)authorversion.pdf (727.78 KB)
Accepted version
Author(s)
Busse, Frank
Nowack, Martin
Cadar, Cristian
Type
Conference Paper
Abstract
When symbolic execution is used to analyse real-world applications,it often consumes all available memory in a relatively short amountof time, sometimes making it impossible to analyse an applicationfor an extended period. In this paper, we present a technique thatcan record an ongoing symbolic execution analysis to disk andselectively restore paths of interest later, making it possible to runsymbolic execution indefinitely.To be successful, our approach addresses several essential re-search challenges related to detecting divergences on re-execution,storing long-running executions efficiently, changing search heur-istics during re-execution, and providing a global view of the storedexecution. Our extensive evaluation of 93 Linux applications showsthat our approach is practical, enabling these applications to runfor days while continuing to explore new execution paths.
Date Issued
2020-07
Date Acceptance
2020-04-17
Citation
2020, pp.63-74
Publisher
ACM
Start Page
63
End Page
74
Copyright Statement
© 2020 Copyright held by the owner/author(s). Publication rights licensed to ACM.
Sponsor
Engineering & Physical Science Research Council (EPSRC)
DSO National Laboratories
Engineering & Physical Science Research Council (EPSRC)
European Research Council (ERC)
Identifier
https://dl.acm.org/doi/abs/10.1145/3395363.3397360
Grant Number
EP/N007166/1
DSOCO16080
EP/R011605/1
819141
Source
29th ACM SIGSOFT International Symposium on Software Testing and Analysis
Publication Status
Published
Start Date
2020-07-18
Finish Date
2020-07-22
Coverage Spatial
Los Angeles/Virtual , CA , USA
Date Publish Online
2020-07-01