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.
Subject groups
-
Mathematics
Computer science (excl engineering aspects)
-
Engineering and Materials Science
Computer engineering (including software)
