A probabilistic separation logic

Gilles Barthe, Justin Hsu, Kevin Liao. A probabilistic separation logic. Proceedings of the ACM on Programming Languages, 4(POPL), 2020. [doi]