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