Jan Smans, Bart Jacobs, Frank Piessens, Wolfram Schulte: Automatic verification of Java programs with dynamic frames. Formal Aspects Comput. 22(3-4): 423-457 (2010)