Charlton, N. and Reus, B. (2009) “A decidable class of verification conditions for programs with higher order store”, Electronic Communications of the EASST, 23. doi: 10.14279/tuj.eceasst.23.318.