Symbolic execution for randomized programs
Symbolic execution for randomized programs
复制标题
DOI：
10.1145/3563344
复制
发表时间：
2022-09
影响因子：
--
通讯作者：
Zachary J. Susag;Sumitra Lahiri;Justin Hsu;Subhajit Roy
中科院分区：
文献类型：
--
作者：
Zachary J. Susag;Sumitra Lahiri;Justin Hsu;Subhajit Roy
我们提出了一个符号执行方法的程序，可以绘制随机样本。与现有的工作相比，我们的方法可以验证未知输入的随机程序，并可以证明在所有可能的输入上普遍量化的概率属性。我们的技术增加了标准的符号执行与一类新的概率符号变量，这代表了随机抽签的结果，并计算符号表达式表示采取个别路径的概率。我们实现了我们的方法顶部的KLEE符号执行引擎旁边的多个优化，并使用它来证明属性的概率和预期值的一系列具有挑战性的案例研究写在C++，包括Freivalds算法，随机快速排序，和随机属性测试算法的单调性。我们评估我们的方法对Psi，一个精确的概率符号推理引擎，和风暴，概率模型检查器，并表明我们的方法显着优于这两种工具。
We propose a symbolic execution method for programs that can draw random samples. In contrast to existing work, our method can verify randomized programs with unknown inputs and can prove probabilistic properties that universally quantify over all possible inputs. Our technique augments standard symbolic execution with a new class of probabilistic symbolic variables, which represent the results of random draws, and computes symbolic expressions representing the probability of taking individual paths. We implement our method on top of the KLEE symbolic execution engine alongside multiple optimizations and use it to prove properties about probabilities and expected values for a range of challenging case studies written in C++, including Freivalds’ algorithm, randomized quicksort, and a randomized property-testing algorithm for monotonicity. We evaluate our method against Psi, an exact probabilistic symbolic inference engine, and Storm, a probabilistic model checker, and show that our method significantly outperforms both tools.