Towards Algebraic Separation Logic

in: Universität Augsburg Technical Report, Institute of Computer Science, University of Augsburg, June 2009

Abstract:
We present an algebraic approach to separation logic. In particular, we give algebraic characterisations for all constructs of separation logic like assertions and commands. 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.

Downloads:

• Towards Algebraic Separation Logic  -  (tr-2009-12_dan_hoe_moe.pdf, 736 KB)