A Decision Procedure for Separation Logic in SMT

TL;DR

This paper introduces a complete decision procedure for quantifier-free Separation Logic, integrated into an SMT solver, enabling more effective reasoning about heap-manipulating programs with data.

Contribution

It provides the first complete decision procedure for the entire quantifier-free fragment of Separation Logic over complex data domains, implemented within an SMT solver.

Findings

Prototype integrated into CVC4 SMT solver.

Preliminary evaluation shows potential for theorem proving and model checking.

Procedure handles heaplets with multi-sorted data domains.

Abstract

This paper presents a complete decision procedure for the entire quantifier-free fragment of Separation Logic ($\seplog$) interpreted over heaplets with data elements ranging over a parametric multi-sorted (possibly infinite) domain. The algorithm uses a combination of theories and is used as a specialized solver inside a DPLL($T$) architecture. A prototype was implemented within the CVC4 SMT solver. Preliminary evaluation suggests the possibility of using this procedure as a building block of a more elaborate theorem prover for SL with inductive predicates, or as back-end of a bounded model checker for programs with low-level pointer and data manipulations.