Professor Michael Gordon FRS
Michael Gordon was internationally renowned for his work on the formal verification of the design of computer hardware, that is to say, the demonstration with the rigour of formal logic that an implementation specification relates correctly to a functional specification. He took this subject from a gleam in the eye of the theorist he then was to one which is applied to real circuits for real purposes. The verification by Michael and Avra Cohn of the Viper microprocessor circuit was a landmark effort. His logic system, HOL, is in use as far away as Beijing; it is a major factor in endeavours to make possible the construction of computer systems for safety-critical and high-integrity applications.
Professor Michael Gordon FRS died on 22 August 2017.
Interests and expertise