Statistical symbolic execution with informed sampling
- 11 November 2014
- conference paper
- conference paper
- Published by Association for Computing Machinery (ACM) in Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering
- p. 437-448
- https://doi.org/10.1145/2635868.2635899
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 limitsKeywords
This publication has 28 references indexed in Scilit:
- Bayesian statistical model checking with application to Stateflow/Simulink verificationFormal Methods in System Design, 2013
- Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysisAutomated Software Engineering, 2013
- A formal approach to adaptive software: continuous assurance of non-functional requirementsFormal Aspects of Computing, 2012
- Numerical vs. statistical probabilistic model checkingInternational Journal on Software Tools for Technology Transfer, 2006
- Effective lattice point counting in rational convex polytopesJournal of Symbolic Computation, 2004
- KoratACM SIGSOFT Software Engineering Notes, 2002
- Symbolic execution and program testingCommunications of the ACM, 1976
- A Retrospective and Prospective Survey of the Monte Carlo MethodSIAM Review, 1970
- Probability Inequalities for Sums of Bounded Random VariablesJournal of the American Statistical Association, 1963
- Sequential Tests of Statistical HypothesesThe Annals of Mathematical Statistics, 1945