Algebraic Separation Logic

Select |




Print


Dang, Han-Hing; Möller, Bernhard; Höfner, Peter

Dang, Han-Hing; Möller, Bernhard; Höfner, Peter


2011-06-01


Journal Article


The Journal of Logic and Algebraic Programming


80


6


221-247


We present an algebraic approach to separation logic. In particular, we give an algebraic characterisation for assertions of separation logic, discuss different classes of assertions and prove abstract laws fully algebraically. After that, we use our algebraic framework to give a relational semantics of the commands of a simple programming language associated with separation logic. On this basis we prove the frame rule in an abstract and concise way. We also propose a more general version of separating conjunction which leads to a frame rule that is more general and easier to prove. For this we show how to algebraically formulate the requirement that a command preserves certain variables. The algebraic view does not only yield new insights on separation logic but also shortens proofs due to a point free representation. It is largely first-order and hence enables the use of off-the-shelf automated theorem provers for verifying properties at an abstract level.


separation logic; algebra


https://doi.org/10.1016/j.jlap.2011.04.003


http://www.sciencedirect.com/science/article/pii/S1567832611000142


nicta:4802


Dang, Han-Hing; Möller, Bernhard; Höfner, Peter. Algebraic Separation Logic. The Journal of Logic and Algebraic Programming. 2011-06-01; 80(6):221-247. https://doi.org/10.1016/j.jlap.2011.04.003



Loading citation data...

Citation counts
(Requires subscription to view)