Range Allocation for Separation Logic

Separation Logic consists of a Boolean combination of predicates of the form v _i ≥ v _j + c where c is a constant and v _i ,v _j are variables of some ordered infinite type like real or integer. Any equality or inequality can be expressed in this logic. We propose a decision procedure for Separation Logic based on allocating small domains (ranges) to the formula’s variables that are sufficient for preserving satisfiability. Given a Separation Logic formula φ, our procedure constructs the inequalities graph of φ, based on φ’s predicates. This graph represents an abstraction of the formula, as there are many formulas with the same set of predicates. Our procedure then analyzes this graph and allocates a range to each variable that is adequate for all of these formulas. This approach of finding small finite ranges and enumerating them symbolically is both theoretically and empirically more efficient than methods based on case-splitting or reduction to Propositional Logic. Experimental results show that the state-space (that is, the number of assignments that need to be enumerated) allocated by our procedure is frequently exponentially smaller than previous methods.