Professor Tom Melham

Professor of Computer Science; Fellow of Balliol College


Professor Melham’s research focuses on mathematical methods for assuring quality and correctness of hardware and software. For many years, he has worked closely with leading companies in microelectronics design 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.


  • Programming language semantics
  • Applications of formal logic
  • Mechanised reasoning
  • Model checking and theorem proving
  • Firmware verification
  • Software verification
  • Automated verification
  • Metacomputation