An efficient decision procedure for imperative tree data structures
T. Wies, M. Muñiz, V. Kuncak, in:, Springer, 2011, pp. 476–491.