Statistical symbolic execution with informed sampling
Statistical symbolic execution with informed sampling
复制标题
具有知情抽样的统计符号执行
DOI：
10.1145/2635868.2635899
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
J. Geldenhuys
中科院分区：
文献类型：
--
作者：
A. Filieri;C. Păsăreanu;W. Visser;J. Geldenhuys
符号执行技术最近被提出来用于程序的概率分析。这些技术试图量化到达感兴趣的节目事件的可能性，断言违规行为。它们有许多有前途的应用，但由于高计算需求而具有可扩展性问题。为了解决这一挑战，我们提出了一种统计符号执行技术，执行Monte Carlo抽样的符号程序路径，并使用所获得的信息贝叶斯估计和假设检验的概率达到目标事件。为了加快统计分析的收敛速度，我们提出了知情采样，这是一种迭代的符号执行，它首先探索具有高统计意义的路径，从状态空间中修剪它们，并引导执行不太可能的路径。该技术结合了贝叶斯估计与部分精确分析的修剪路径，导致可证明的改进收敛的统计分析。我们已经实现了统计符号执行与知情的采样中的符号路径工具。我们的实验表明，知情的抽样获得更精确的结果，收敛速度比纯粹的统计分析，也可能是更有效的比一个确切的符号分析。当后者不终止时，具有通知采样的符号执行可以在相同的时间和内存限制下给出有意义的结果。
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.