Gast, H.; Trieflinger, J. High-Level Proofs about Low-Level Programs. eceasst 2009, 23.