Martin Brain, Cristina David, Daniel Kroening, Peter Schrammel: Model and Proof Generation for Heap-Manipulating Programs. ESOP 2014: 432-452