Statistical symbolic execution with informed sampling
File(s)
Accepted version
Author(s)
Filieri, A
P uas uareanu, CS
Visser, W
Geldenhuys, J
Type
Conference Paper
Abstract
Symbolic execution techniques have been proposed recently for the probabilistic analysis of programs. These techniques seek to quantify the likelihood of reaching program events of interest, e.g., assert violations. They have many promising applications but have scalability issues due to high computational demand. To address this challenge, we propose a statistical symbolic execution technique that performs Monte Carlo sampling of the symbolic program paths and uses the obtained information for Bayesian estimation and hypothesis testing with respect to the probability of reaching the target events. To speed up the convergence of the statistical analysis, we propose Informed Sampling, an iterative symbolic execution that first explores the paths that have high statistical significance, prunes them from the state space and guides the execution towards less likely paths. The technique combines Bayesian estimation with a partial exact analysis for the pruned paths leading to provably improved convergence of the statistical analysis. We have implemented statistical symbolic execution with informed sampling in the Symbolic PathFinder tool. We show experimentally that the informed sampling obtains more precise results and converges faster than a purely statistical analysis and may also be more efficient than an exact symbolic analysis. When the latter does not terminate symbolic execution with informed sampling can give meaningful results under the same time and memory limits.
Date Issued
2014-11-16
Date Acceptance
2014-11-16
Citation
Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2014, pp.437-448
ISBN
978-1-4503-3056-5
Publisher
ACM
Start Page
437
End Page
448
Journal / Book Title
Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering
Copyright Statement
© ACM 2014. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, http://dx.doi.org/10.1145/2635868.2635899
Source
22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering
Publication Status
Published
Start Date
2014-11-16
Finish Date
2014-11-21
Coverage Spatial
Hong Kong