Simulating Microprocessors from Formal Specifications. - Kelly M. Hall; Phillip J. Windley (TPHOLs, 1992)