H. Gast and J. Trieflinger, “High-level Proofs about Low-level Programs”, eceasst, vol. 23, Dec. 2009.