Gast, H. and Trieflinger, J. (2009) “High-level Proofs about Low-level Programs”, Electronic Communications of the EASST, 23. doi: 10.14279/tuj.eceasst.23.319.