A Discipline for Program Verification Based on Backpointers and Its Use in Observational Disjointness. - Ioannis T. Kassios; Eleftherios Kritikos (ESOP, 2013)