Magnus O. Myreen, Anthony C. J. Fox, Michael J. C. Gordon: Hoare Logic for ARM Machine Code. FSEN 2007: 272-286