References & Citations
Computer Science > Programming Languages
Title: A Separation Logic for Concurrent Randomized Programs
(Submitted on 8 Feb 2018 (v1), last revised 21 Nov 2018 (this version, v2))
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.
Submission history
From: Joseph Tassarotti [view email][v1] Thu, 8 Feb 2018 16:29:43 GMT (98kb,D)
[v2] Wed, 21 Nov 2018 16:12:53 GMT (99kb,D)
Link back to: arXiv, form interface, contact.