Proof search for propositional abstract separation logics via labelled sequents
Zhé Hóu, Ranald Clouston, Rajeev Prabhakar Goré, Alwen Tiu · 2014
Abstract separation logics are a family of extensions of Hoare logic for reasoning about programs that mutate memory. These logics are "abstract" because they are independent of any particular concrete memory model. Their assertion languages, called propositional abstract separation logics, extend the logic of (Boolean) Bunched Implications (BBI) in various ways.