Targeted program transformations for symbolic execution
File(s)
Accepted version
Author(s)
Cadar, C
Type
Conference Paper
Abstract
Semantics-preserving program transformations, such as refactorings and optimisations, can have a significant impact on the effectiveness of symbolic execution testing and analysis. Furthermore, semantics-preserving transformations that increase the performance of native execution can in fact decrease the scalability of symbolic execution. Similarly, semantics-altering transformations, such as type changes and object size modifications, can often lead to substantial improvements in the testing effectiveness achieved by symbolic execution in the original program. As a result, we argue that one should treat program transformations as first-class ingredients of scalable symbolic execution, alongside widely-accepted aspects such as search heuristics and constraint solving optimisations. First, we propose to understand the impact of existing program transformations on symbolic execution, to increase scalability and improve experimental design and reproducibility. Second, we argue for the design of testability transformations specifically targeted toward more scalable symbolic execution.
Date Issued
2015-08-30
Date Acceptance
2015-07-01
Citation
2015
Publisher
ACM
Copyright Statement
© 2015 The Authors
Sponsor
Engineering & Physical Science Research Council (EPSRC)
Identifier
https://dl.acm.org/doi/10.1145/2786805.2803205
Grant Number
EP/L002795/1
Source
European Software Engineering Conference / Symposium on the Foundations of Software Engineering New Ideas Track (ESEC/FSE NI 2015)
Subjects
Science & Technology
Technology
Computer Science, Software Engineering
Computer Science, Theory & Methods
Engineering, Electrical & Electronic
Computer Science
Engineering
Testability transformations
dynamic symbolic execution
Publication Status
Published
Start Date
2015-08-30
Finish Date
2015-09-04
Coverage Spatial
Bergamo, Italy
Date Publish Online
2015-08