Tom Melham - Short Biography

Tom Melham is a Professor of Computer Science at the University of Oxford and a Fellow of Balliol College, where he is Tutor in Computation. He received his PhD from the University of Cambridge in 1990 for his foundational research in computer-aided formal proof and its applications to microelectronics circuit design. Melham was also a co-developer of the original HOL theorem prover for higher order logic at Cambridge. In 1993 he joined the Computing Science Department at Glasgow University and was appointed to a Professorship of Computing Science at Glasgow in 1998, before moving to Oxford in 2002. During 2012-15, he was Associate Head of Oxford's Mathematical, Physical and Life Sciences Division and served for ten years from 2010 as Praefectus of Holywell Manor. He was elected a Fellow of the Royal Society of Edinburgh in 2002 and a Fellow of the British Computer Society in 2015.

Melham's research is focussed on mathematical methods for assuring quality and correctness of hardware and software. For many years, he has worked closely with leading companies in the semiconductor industry on advanced tools and methods for microchip design validation. His research contributions include publications on theorem proving, software architectures for formal reasoning tools, combined model checking and theorem proving, industrial-scale hardware verification, abstraction techniques, integrating formal verification into hardware design methodologies, hardware/software co-design and co-validation, validation of low-level firmware, and validation and analysis of System-on-Chip designs.

Tom Melham, last updated Thu Oct 1 06:20:43 BST 2020