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