About
I am a research manager in the area of 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.
Recent Papers
- 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 (to appear).
Recent Talks
- 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
Recent Awards
- ICSE 2017 Most Influential Paper Award: Carlos Pacheco, Shuvendu K. Lahiri, Michael D. Ernst, and Thomas Ball: Feedback-Directed Random Test Generation, ICSE-29, 2007
Other Writing
- 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
Projects
Publications
Videos
Other
Tools
- 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
Recent Talks
- 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
Awards
- 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.
Recent Service
- 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
History
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“.
