  Constrained Horn Clauses (CHCs) are an intermediate program representation
that can be generated by several verification tools, and that can be processed
and solved by a number of Horn solvers. One of the main challenges when using
CHCs in verification is the encoding of heap-allocated data-structures: such
data-structures are today either represented explicitly using the theory of
arrays, or transformed away with the help of invariants or refinement types,
defeating the purpose of CHCs as a representation that is language-independent
as well as agnostic of the algorithm implemented by the Horn solver. This paper
presents an SMT-LIB theory of heap tailored to CHCs, with the goal of enabling
a standard interchange format for programs with heap data-structures. We
introduce the syntax of the theory of heap, define its semantics in terms of
axioms and using a reduction to SMT-LIB arrays and data-types, and discuss its
properties and outline possible extensions and future work.
