Range Allocation for Separation Logic

11 years 2 months ago
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...
Muralidhar Talupur, Nishant Sinha, Ofer Strichman,
Added 01 Jul 2010
Updated 01 Jul 2010
Type Conference
Year 2004
Where CAV
Authors Muralidhar Talupur, Nishant Sinha, Ofer Strichman, Amir Pnueli
Comments (0)