Dr Thomas Ball

Honorary Professor

Research Overview

Thomas (Tom) Ball is a co-founder of the influential SLAM software model checking project and creation of the Static Driver Verifier tool for finding defects in Windows device drivers. Tom is a 2011 ACM Fellow for ‘contributions to software analysis and defect detection’. As a manager at Microsoft Research, he nurtured research areas such as automated theorem proving, program testing/verification and empirical software engineering, and their application to industrial scale software engineering problems. Since 2015, he worked to bring the BBC micro:bit to market (more than 10 million worldwide to date) and establish the Microsoft MakeCode platform for supporting CS education efforts. Most recently, he worked on Jacdac, a new plug-and-play system for microcontrollers. His current project is MicroCode, a way to program micro:bits without a separate computer.

Selected Publications

Symbolic Automata: Omega-Regularity Modulo Theories
Veanes, M., Ball, T., Ebner, G., Zhuchko, E. 9/01/2025 In: Proceedings of the ACM on Programming Languages. 9, p. 33-66. 34 p.
Journal article

Jacdac: Service-Based Prototyping of Embedded Systems
Ball, T., de Halleux, P., Devine, J., Hodges, S., Moskal, M. 20/06/2024 In: Proceedings of the ACM on Programming Languages. 8, PLDI, p. 692-715. 24 p.
Journal article

Micro:bit Apps
01/01/2024 → …
Research

  • Education (SCC)
  • Micro:bit Innovation and Research Lab
  • Pervasive Systems (SCC)
  • SCC (Software Engineering)