Dr Thomas Ball
Honorary ProfessorResearch 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.
PhD Supervision Interests
micro:bit apps
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
All Publications
Micro:bit Apps
01/01/2024 → …
Research
Micro:bit Innovation and Research Lab
- Education (SCC)
- Micro:bit Innovation and Research Lab
- Pervasive Systems (SCC)
- SCC (Software Engineering)