A separation logic for concurrent randomized programs

Joseph Tassarotti, Robert Harper

Research output: Contribution to journalArticlepeer-review


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.

Original languageEnglish (US)
Article number64
JournalProceedings of the ACM on Programming Languages
Issue numberPOPL
StatePublished - Jan 2019


  • Concurrency
  • Probability
  • Separation logic

ASJC Scopus subject areas

  • Software
  • Safety, Risk, Reliability and Quality

Cite this