In recent work, we have proposed an SMT-LIB theory of heap tailored
  to Horn-clause verification. The theory makes it possible to lift
  verification approaches for heap-allocated data-structures to a
  language-independent level, and this way factor out the treatment of
  heap in verification tools. This paper gives an overview of the
  theory, and presents ongoing research on decision and interpolation
  procedures.