Compositional Solution Space Quantification for Probabilistic Software Analysis
Compositional Solution Space Quantification for Probabilistic Software Analysis
复制标题
DOI：
10.1145/2594291.2594329
复制
发表时间：
2014-06-01
影响因子：
--
通讯作者：
Visser, Willem
中科院分区：
文献类型：
--
作者：
Borges, Mateus;Filieri, Antonio;Visser, Willem
概率软件分析旨在量化目标事件在程序执行期间发生的可能性。当前的方法依赖于符号执行来识别到达目标事件的条件，并尝试量化满足这些条件的输入域的分数。精确的量化通常限于线性约束，而通过统计方法通常只能提供近似解。然而，统计方法可能无法收敛到一个可接受的精度在一个合理的时间内，我们提出了一个组合的统计方法的有效量化的解决方案空间的任意复杂的约束有界浮点域。该方法利用区间约束传播，通过将采样集中在包含所寻求的解决方案的输入域的区域上来提高估计的准确性。初步的实验表明，显着改善以前的方法，无论是在结果的准确性和分析时间。
Probabilistic software analysis aims at quantifying how likely a target event is to occur during program execution. Current approaches rely on symbolic execution to identify the conditions to reach the target event and try to quantify the fraction of the input domain satisfying these conditions. Precise quantification is usually limited to linear constraints, while only approximate solutions can be provided in general through statistical approaches. However, statistical approaches may fail to converge to an acceptable accuracy within a reasonable time.We present a compositional statistical approach for the efficient quantification of solution spaces for arbitrarily complex constraints over bounded floating-point domains. The approach leverages interval constraint propagation to improve the accuracy of the estimation by focusing the sampling on the regions of the input domain containing the sought solutions. Preliminary experiments show significant improvement on previous approaches both in results accuracy and analysis time.