Heap and data structures represent one of the biggest challenges
  when applying model checking to the analysis of software programs:
  in order to verify (unbounded) safety of a program, it is typically
  necessary to formulate quantified inductive invariants that state
  properties about an unbounded number of heap locations. Methods like
  Craig interpolation, which are commonly used to infer invariants in
  model checking, are often ineffective when a heap is involved. To
  address this challenge, we introduce a set of new proof and program
  transformation rules for verifying object-oriented programs with the
  help of \emph{space invariants,} which (implicitly) give rise to
  quantified invariants. Leveraging advances in Horn solving, we show
  how space invariants can be derived fully automatically, and how
  the framework can be used to effectively verify safety of Java
  programs.