A Separation Logic for Concurrent Randomized Programs
arXiv:1802.02951 · doi:10.1145/3290377
Abstract
We present Polaris, a concurrent separation logic with support for probabilistic reasoning. As part of our logic, we extend the idea of coupling, which underlies recent work on probabilistic relational logics, to the setting of programs with both probabilistic and non-deterministic choice. To demonstrate Polaris, we verify a variant of a randomized concurrent counter algorithm and a two-level concurrent skip list. All of our results have been mechanized in Coq.
31 pages. Extended version of POPL 2019 paper
References in corpus (3)
Cited by in corpus (16)
- Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Programs
- Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning
- Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
- A Separation Logic for Negative Dependence
- Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects
- Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
- Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
- A Generic Methodology for the Modular Verification of Security Protocol Implementations (extended version)
- On Algebraic Abstractions for Concurrent Separation Logics
- Tachis: Higher-Order Separation Logic with Credits for Expected Costs
- A Demonic Outcome Logic for Randomized Nondeterminism
- Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning
- Almost-Sure Termination by Guarded Refinement
- Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants
- A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism
- GradInf: Gradient Estimation as Probabilistic Inference