The papers “Generating Inductive Predicates for Symbolic Execution of Pointer-Manipulating Programs” by Christina Jansen, Florian Göbe, and Thomas Noll, and “Generating Abstract Graph-Based Procedure Summaries for Pointer Programs” by Christina Jansen and Thomas Noll have been accepted at ICGT 2014 in York, GB.  The former paper relates two abstraction approaches for pointer programs, graph grammars and separation logic, while the latter presents an interprocedural dataflow analysis to automatically derive graph-based procedure contracts.