An Assertion-Based Program Logic for Probabilistic Programs
An Assertion-Based Program Logic for Probabilistic Programs
复制标题
DOI：
10.1007/978-3-319-89884-1_5
复制
发表时间：
2018-03
期刊：
影响因子：
--
通讯作者：
G. Barthe;Thomas Espitau;Marco Gaboardi;B. Grégoire;Justin Hsu;Pierre-Yves Strub
中科院分区：
文献类型：
--
作者：
G. Barthe;Thomas Espitau;Marco Gaboardi;B. Grégoire;Justin Hsu;Pierre-Yves Strub
我们提出了Ellora，一个健全的和相对完整的基于断言的程序逻辑，并证明其表现力通过验证随机算法的几个经典的例子，使用EasyCrypt证明助手的实现。Ellora为循环和对抗代码提供了新的证明规则，并支持比现有程序逻辑更丰富的断言。我们还表明，Ellora允许方便的推理复杂的概率概念，通过开发一个新的程序逻辑的概率独立性和分布规律，然后顺利地嵌入到Ellora。
We present Ellora, a sound and relatively complete assertion-based program logic, and demonstrate its expressivity by verifying several classical examples of randomized algorithms using an implementation in the EasyCrypt proof assistant. Ellora features new proof rules for loops and adversarial code, and supports richer assertions than existing program logics. We also show that Ellora allows convenient reasoning about complex probabilistic concepts by developing a new program logic for probabilistic independence and distribution law, and then smoothly embedding it into Ellora.