Program verification as probabilistic inference
Program verification as probabilistic inference
复制标题
DOI：
10.1145/1190215.1190258
复制
发表时间：
2007-01-01
影响因子：
--
通讯作者：
Jojic, Nebojsa
中科院分区：
文献类型：
--
作者：
Gulwani, Sumit;Jojic, Nebojsa
在本文中，我们提出了一种新算法来证明程序的前置/后置条件对的有效性或无效性。该算法的灵感源自机器学习社区开发的用于图模型推理的概率推理算法的成功。有效性或无效性证明包括在每个程序点提供可以本地验证的不变量。该算法的工作原理是迭代地随机选择一个程序点并更新当前的抽象状态表示，以使其更加局部一致（相对于相邻点的抽象）。我们证明这个简单的算法有一些有趣的方面：（a）它汇集了前向和后向分析的互补能力； (b) 该算法能够从其可能做出的过度欠近似或过度近似中恢复过来。 （因为该算法不区分前向和后向信息，所以该信息在任何步骤都可能被低估和过度近似。）（c）算法中的随机性确保最终做出正确的更新选择，因为没有单一的确定性策略可以证明适用于任何有趣的程序类别。在我们的实验中，我们使用该算法来证明一个小（但不平凡）示例的正确性。此外，我们还凭经验说明了该算法的几个重要属性。
In this paper, we propose a new algorithm for proving the validity or invalidity of a pre/postcondition pair for a program. The algorithm is motivated by the success of the algorithms for probabilistic inference developed in the machine learning community for reasoning in graphical models. The validity or invalidity proof consists of providing an invariant at each program point that can be locally verified. The algorithm works by iteratively randomly selecting a program point and updating the current abstract state representation to make it more locally consistent (with respect to the abstractions at the neighboring points). We show that this simple algorithm has some interesting aspects: (a) It brings together the complementary powers of forward and backward analyses; (b) The algorithm has the ability to recover itself from excessive under-approximation or over-approximation that it may make. (Because the algorithm does not distinguish between the forward and backward information, the information could get both under-approximated and over-approximated at any step.) (c) The randomness in the algorithm ensures that the correct choice of updates is eventually made as there is no single deterministic strategy that would provably work for any interesting class of programs. In our experiments we use this algorithm to produce the proof of correctness of a small (but non-trivial) example. In addition, we empirically illustrate several important properties of the algorithm.