N. Charlton and B. Reus, “A decidable class of verification conditions for programs with higher order store”, eceasst, vol. 23, Dec. 2009.