Charlton, N.; Reus, B. A Decidable Class of Verification Conditions for Programs With Higher Order Store. ECEASST 2009, 23.