论文标题
概率：概率验证的声音和完整的证明规则
ProbTA: A sound and complete proof rule for probabilistic verification
论文作者
论文摘要
我们提出了一个声音和完整的证明规则，以定量分析概率程序的违规概率。我们的方法在控制流随机性样式中扩展了痕量抽象的技术，与采用数据随机性样式的痕量抽象和概率验证相比。在我们的方法中，通过将程序分解为不同的痕迹模块，证明或反驳了程序规范。精确的定量分析是通过提出桥接程序验证和概率理论的新型模型来实现的。基于证明规则，我们通过CEGAR提出了一种新的自动化算法，该算法涉及多个技术问题，在非探针痕迹抽象和基于数据随机性的方法中毫无前身。
We propose a sound and complete proof rule ProbTA for quantitative analysis of violation probability of probabilistic programs. Our approach extends the technique of trace abstraction with probability in the control-flow randomness style, in contrast to previous work of combining trace abstraction and probabilisitic verification which adopts the data randomness style. In our method, a program specification is proved or disproved by decomposing the program into different modules of traces. Precise quantitative analysis is enabled by novel models proposed to bridge program verification and probability theory. Based on the proof rule, we propose a new automated algorithm via CEGAR involving multiple technical issues unprecedented in non-probabilistic trace abstraction and data randomness-based approach.
