Safety, Relative Tightness and the Probabilistic Frame Rule

Janez Ignacij Jereb, Alex Simpson

Probabilistic separation logic offers an approach to reasoning about imperative probabilistic programs in which a separating conjunction is used as a mechanism for expressing indep…