Proof search for prepositional abstract separation logics via labelled sequents

摘要

Pointers and sharing have always been difficult problems in program verification, and several extensions to Hoare logic have been proposed and investigated over the decades. A very promising, quite recent approach is Reynolds' separation logic, which draws on experiences in substruc-tural or resource-sensitive logics having connectives different from classical logic. This paper is concerned with proof search in the propo-sitional kernel of abstract separation logics (PASL), which have algebraic structures as models that abstract away the details of a concrete memory model. These abstract separation logics are in several ways similar to the logic of Boolean bunched implications (BBI).