Darren Lee Buttle: Verification of compiled code. University of York, UK 2001