2024/06/02 by Janine Lohse, Deepak Garg, Lohse, Janine +1 · 1 citation
Decision Sciences · #FOS: Computer and information sciences #Programming Languages (cs.PL) #Simulation Techniques and Applications
paper · pdf · doi:10.48550/arxiv.2406.00884
openalex publication_date 2024/06/02 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.