Range Allocation for Separation Logic

Abstract. Separation Logic consists of a Boolean combination of predicates of the form vi ≥ vj +c where c is a constant and vi, vj 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 ϕ, 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 casesplitting or reduction to Propositional Logic. Experimenta...

• Type: Conference
• Year: 2004
• Where: CAV
• Authors: Muralidhar Talupur, Nishant Sinha, Ofer Strichman, Amir Pnueli
• Keywords: CAV 2004, Formal Methods, Procedure, Separation Logic, Separation Logic Formula