Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Programs

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen +2

We present quantitative separation logic ($\mathsf{QSL}$). In contrast to classical separation logic, $\mathsf{QSL}$ employs quantities which evaluate to real numbers instead of pr…