A Constraint Solver for Heaps with Separation
Gregory Duck, Joxan Jaffar and Nicolas Koh
Abstract
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.