I work in the area of programming languages and software engineering in MSR’s Redmond Lab. My research interests are in how combinations of static/dynamic program analysis, model checking and theorem proving techniques can help improve the correctness and reliability of programs. I’ve been working recently on Microsoft MakeCode, a new platform for bringing physical computing to everyone, based on our experience with the BBC micro:bit. See my papers for more details.
CHI 2018 – ARcadia: A Rapid Prototyping Platform for Real-time Tangible Interfaces. Annie Kelly, R. Benjamin Shapiro, Jonathan de Halleux, Thomas Ball. April 2018
LCTES 2018 – MakeCode and CODAL: Intuitive and Efficient Embedded Systems Programming for Education. James Devine, Joe Finney, Peli de Halleux, Michal Moskal, Thomas Ball, Steve Hodges. June 2018
Invited Talk: Formal Methods and Tools for Distributed Systems, NUS Computer Science Research Week 2019, January 2019 [Slides]
Keynote: Push, Pull, Partner A Few Models for Working with Industry, International Conference on Software Architecture, May 2018 [Slides]
Northwest C++ User’s Group – Microsoft MakeCode: from C++ to TypeScript and Blockly (and Back)
[ Video | Slides ]
Invited talk “Physical Computing for Everyone” at UCSD Design Lab, October 11, 2017
Keynote: “Formal Methods at Scale in Microsoft” at Software-Centric Systems Conference, Eindhoven, October 4, 2017
Keynote “Physical Computing for Everyone”, ICSE Software Engineering Education and Training, May 2017
Blog: Microsoft Research and the Industrial Research Cycle
Microsoft Touch Develop and the BBC micro:bit, Thomas Ball, Jonathan Protzenko, Judith Bishop, Michal Moskal, Jonathan de Halleux, Michael Braun, Steve Hodges, Clare Riley, ICSE 2016
CloudSDV Enabling Static Driver Verifier Using Microsoft Azure, Rahul Kumar, Thomas Ball, Jakob Lichtenberg, Nate Deisinger, Apoorv Upreti, Chetan Bansal: IFM 2016: 523-536
Teach foundational language principles. Thomas Ball, Benjamin Zorn. Commun. ACM 58(5): 30-31 (2015)
Beyond Open Source: The Touch Develop Cloud-Based Integrated Development Environment. MOBILESoft 2015: 83-93
Deconstructing Dynamic Symbolic Execution. Dependable Software Systems Engineering 2015: 26-41
- TouchDevelop on GitHub
- Static Driver Verifier Research Platform released
- Source code of CHESS (and Alpaca test framework) released on codeplex
- Source code of Randoop for .NET released
- TouchDevelop: Scripting Mobile+Cloud Apps via Mobile+Cloud, Rutgers University, April 22, 2014
- TouchDevelop: Productive Scripting on and for Touch-based Devices and Web Services, Cornell University, Sept 12 2013
- TouchDevelop Tutorial at PLDI 2013, June 2013
- Advances in Automated Theorem Proving, Distinguished Lecture, University British Columbia, October 2012
- May 2011: A Plague of Plug-ins (Keynote, Tools as Plug-ins Workshop, ICSE 2011)
- June 2010: Concurrency Testing with CHESS (Learning From eXperience 2010)
- Mar 2010: Preemption Sealing for Efficient Concurrency Testing [pdf] at Portland State University
- Oct 2009: The SMT “Big Bang”: Applications of Z3 in Microsoft
- May 2009: Program Analysis 2.0 [pdf] at UIUC‘s UPCRC Research Seminar
- May 2009: A Brief History of Software [pdf], at Mining Software Repositories Working Conference
- January 2008: 30 Years of Abstract Interpretation [slides,text], in honour of Patrick Cousot
- 2011 ACM Fellow: For contributions to software analysis and defect detection.
- The 2011 CAV Award is given to Thomas Ball and Sriram Rajamani for their contributions to software model checking, specifically the development of the SLAM/SDV software model checker that successfully demonstrated computer-aided verification techniques on real programs
- Most Influential PLDI Paper award for Automatic Predicate Abstraction of C Programs, Thomas Ball, Rupak Majumdar, Todd D. Millstein, Sriram K. Rajamani, PLDI 2001. The first conference paper from the SLAM project!
- Exploiting Hardware Performance Counters with Flow and Context Sensitive Profiling won the Most Influential PLDI Paper Award, PLDI 2007.
- Distinguished paper at OOPSLA 2011: Sebastian Burckhardt, Daan Leijen, Caitlin Sadowski, Jaeheon Yi, and Thomas Ball, Two for the Price of One: A Model for Parallel and Incremental Computation
- IEEE Software article “Righting Software” was selected by Software’s editorial and advisory boards as one of the 25th-Anniversary Top Picks for full-length, peer-reviewed articles.
- PCs 2013: International Conference on Software Testing, Verification and Validation; NASA Formal Methods Symposium; ICSE 2013 New Ideas and Emerging Results Track; 2012: Off the Beaten Track: Underrepresented Problems for Programming Language Researchers (POPL 2012 Workshop),
- Co-chair, Theoretical Computer Science 2012.
- General Chair, POPL 2011. Here’s my report on how it went.
- 2008 Marktoberdorf Summer School on “Engineering Methods and Tools for Software Safety and Security” (August ’08)
- LASER Summer School on Software Engineering (2007)
- On the Design and Implementation of Static Analysis Tools at the University of Washington (2007)
- FLoC 2006 conference co-chair
- Program chair of PLDI 2006, program co-chair of CAV 2006
I grew up in Summit, NJ, where my claim to fame was writing a game for the Apple ][ called Falcons in 1980 with high school pal Eric Varsanyi (see The Giant List of Classic Game Programmers). I attended Cornell University (B.A. 1987), and the University of Wisconsin-Madison (Ph.D. 1993). From 1993-1999, I was at Bell Labs in Naperville, IL in the (now defunct) Software Production Research Department. After 12 years as a Midwesterner, I had had enough. Now I live in Mercer Island, WA. I have sung in various Unitarian Universalist choirs, play e-bass (mainly jazz, blues, some rock ‘n roll) and piano. I now play in a band called the “The Middle Third“.