Towards Algebraic Separation Logic

erschienen 2009 in R. Berghammer, A. M. Jaoua, B. Möller (eds.): Relations and Kleene Algebra in Computer Science, LNCS 5827.
pp. 59-72, 2009.

Abstract:
We present an algebraic approach to separation logic. In particular, we give algebraic characterisations for all constructs of separation logic. The algebraic view does not only yield new insights on separation logic but also shortens proofs and enables the use of automated theorem provers for verifying properties at a more abstract level.