He is a Professor in the Department of Computer Science at the University of Bristol and founder of XMOS Semiconductor, serving until February 2014 as the chief technology officer.
When Inmos was formed in 1978, May joined to work on microcomputer architecture, becoming lead architect of the transputer and designer of the associated programming language Occam.
Working closely with Tony Hoare and the Programming Research Group at Oxford University, May introduced formal verification techniques into the design of the T800 floating point unit and the T9000 transputer.
These were some of the earliest uses of formal verification in microprocessor design, involving specifications, correctness preserving transformations and model checking, giving rise to the initial version of the FDR checker developed at Oxford.
In 1990, May received an Honorary DSc from the University of Southampton, followed in 1991 by his election as a Fellow of The Royal Society and the Clifford Paterson Medal and Prize of the Institute of Physics in 1992.