A Constraint Solver for Heaps with Separation

Gregory Duck, Joxan Jaffar and Nicolas Koh


This paper introduces a constraint language $\HH$ for \emph{finite partial maps} (a.k.a. \emph{heaps}) that incorporates the notion of \emph{separation} from \emph{Separation Logic}. The motivation behind $\HH$ is reasoning over heap manipulating programs using constraint-based symbolic execution. For this we present a modest extension of \emph{Hoare Logic} that inherits many of the benefits from Separation Logic, such as local reasoning, but encodes heap operations as $\HH$-formulae. Next we present a sound and complete solving algorithm for quantifier-free $\HH$-formulae, and an implementation that has been integrated into a \emph{Satisfiability Modulo Theories} (SMT) framework. We experimentally evaluate the implementation against \emph{Verification Conditions} (VCs) generated from symbolic execution of large programs. In particular, we mitigate the \emph{path explosion problem} using subsumption via interpolation.