F. Stappers and M. Reniers, “Verification of safety requirements for program code using data abstraction”, eceasst, vol. 23, Dec. 2009.