We present ExpIris, a separation logic framework for the (amortized) expected cost analysis of probabilistic programs. ExpIris is based on Iris, parametric in the language and the cost model, and supports both imperative and functional languages, concurrency, higher-order functions and higher-order state. ExpIris also offers strong support for correctness reasoning, which greatly eases the analysis of programs whose expected cost depends on their high-level behavior. To enable expected cost reasoning in Iris, we build on the expected potential method. The method provides a kind of "currency" that can be used for paying for later operations, and can be distributed over the probabilistic cases whenever there is a probabilistic choice, preserving the expected value due to the linearity of expectations. We demonstrate ExpIris by verifying the expected runtime of a quicksort implementation and the amortized expected runtime of a probabilistic binary counter.

翻译：我们提出了ExpIris，一个用于概率程序（摊销）期望代价分析的分离逻辑框架。ExpIris基于Iris，在语言和代价模型上具有参数化特性，支持命令式和函数式语言、并发、高阶函数以及高阶状态。ExpIris还为正确性推理提供了强大支持，这极大地简化了那些期望代价依赖于其高层行为的程序的分析。为了在Iris中实现期望代价推理，我们基于期望势能方法进行构建。该方法提供了一种可用于支付后续操作的“货币”，并且可以在存在概率选择时将其分配到各个概率分支上，由于期望的线性性质，其期望值得以保持。我们通过验证快速排序实现的期望运行时间和一个概率二进制计数器的摊销期望运行时间，展示了ExpIris的能力。