# A Separation Logic for Concurrent Randomized Programs

arXiv: https://arxiv.org/abs/1802.02951 · HTML: https://mlsanity.com/paper/1802.02951/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 8 Feb 2018.

## Built on by (most cited first, 3 of 3)

- [Formalization of a Stochastic Approximation Theorem](https://mlsanity.com/paper/2202.05959/) (2022)
- [Formalized Hopfield Networks and Boltzmann Machines](https://mlsanity.com/paper/2512.07766/) (2025)
- [GradInf: Gradient Estimation as Probabilistic Inference](https://mlsanity.com/paper/2607.07840/) (2026)

## Abstract (arXiv)

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.