Accelerating array constraints in symbolic execution
File(s)
Accepted version
Author(s)
Perry, DM
Mattavelli, A
Zhang, X
Cadar, C
Type
Conference Paper
Abstract
Despite significant recent advances, the effectiveness of symbolic
execution is limited when used to test complex, real-world software.
One of the main scalability challenges is related to constraint solv-
ing: large applications and long exploration paths lead to complex
constraints, often involving big arrays indexed by symbolic expres-
sions. In this paper, we propose a set of semantics-preserving trans-
formations for array operations that take advantage of contextual
information collected during symbolic execution. Our transforma-
tions lead to simpler encodings and hence better performance in
constraint solving. The results we obtain are encouraging: we show,
through an extensive experimental analysis, that our transforma-
tions help to significantly improve the performance of symbolic
execution in the presence of arrays. We also show that our transfor-
mations enable the analysis of new code, which would be otherwise
out of reach for symbolic execution.
execution is limited when used to test complex, real-world software.
One of the main scalability challenges is related to constraint solv-
ing: large applications and long exploration paths lead to complex
constraints, often involving big arrays indexed by symbolic expres-
sions. In this paper, we propose a set of semantics-preserving trans-
formations for array operations that take advantage of contextual
information collected during symbolic execution. Our transforma-
tions lead to simpler encodings and hence better performance in
constraint solving. The results we obtain are encouraging: we show,
through an extensive experimental analysis, that our transforma-
tions help to significantly improve the performance of symbolic
execution in the presence of arrays. We also show that our transfor-
mations enable the analysis of new code, which would be otherwise
out of reach for symbolic execution.
Date Acceptance
2017-04-29
Publisher
ACM
Copyright Statement
© 2017 the authors
Sponsor
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
Grant Number
EP/N007166/1
EP/L002795/1
Source
International Symposium on Software Testing and Analysis (ISSTA)
Subjects
Science & Technology
Technology
Computer Science, Software Engineering
Computer Science, Theory & Methods
Computer Science
Symbolic execution
Constraint solving
Theory of arrays
Publication Status
Accepted
Start Date
2017-07-10
Finish Date
2017-07-14
Coverage Spatial
Santa Barbara, CA, USA