\begin{abstract}
  We present a concurrent separation logic with support for probabilistic reasoning.
  As part of our logic, we extend the idea of \emph{coupling}, which underlies recent work on probabilistic relational logics,
  to the setting of programs with both probabilistic and non-deterministic choice.
  To demonstrate our logic, 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.

\end{abstract}