I am a research manager in the area of software engineering. 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. See my papers for more details.
- TouchDevelop: Productive Scripting on and for Touch-based Devices and Web Services, Cornell University, Sept 12 2013
- Efficient Modular SAT Solving for IC3, with Say Bayless, Celina Val, Holger Hoos, and Alan Hu, to appear FMCAD 2013
Microsoft Faculty Summit: Modern Programming for and via the Web Browser | video, Shriram Krishnamurthi, Brown University | slides, Steve Lucco, Microsoft | slides, Tom Ball, Microsoft Research | slides, July 2013
- TouchDevelop Tutorial at PLDI 2013, June 2013
- Advances in Automated Theorem Proving, Distinguished Lecture, University British Columbia, October 2012
- Modular and Verified Automatic Program Repair, Thomas Ball, Francesco Logozzo, OOPSLA 2012
- Beyond First-Order Satisfaction: Fixed Points, Interpolants, Automata and Polynomials, Thomas Ball, Nikolaj Bjørner, Leonardo de Moura, Kenneth L. McMillan, Margus Veanes: SPIN 2012
- Type-Directed Completion of Partial Expressions, Daniel Perelman, Sumit Gulwani, Thomas Ball, Dan Grossman, PLDI 2012
- Static Driver Verifier Research Platform released
- Source code of CHESS (and Alpaca test framework) released on codeplex
- Source code of Randoop for .NET released
Sebastian Burckhardt, Daan Leijen, Caitlin Sadowski, Jaeheon Yi, and Thomas Ball, Two for the Price of One: A Model for Parallel and Incremental Computation, in Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA'11), ACM SIGPLAN, Portland, Oregon, 22 October 2011
A Decade of Software Model Checking with SLAM, T. Ball, V. Levin, S. K. Rajamani, Communications of the ACM, Vol. 54. No. 7, 2011, Pages 68-76
- Predictable and Progressive Testing of Multithreaded Code, T. Ball, S. Burckhardt, P. de Halleux, M. Musuvathi, S. Qadeer, IEEE Software, May/June 2011, pp. 75-83
- Practical parallel and concurrent programming, T. Ball, J. Bishop, S. Burckhardt, G. Gopalakrishnan, J. Mayo, M. Musuvathi, S. Qadeer, S. Toub, SIGCSE 2011
- SLAM2: Static Driver Verification with Under 4% False Alarms, T. Ball, E. Bounimova, R. Kumar and V. Levin, FMCAD 2010
- Efficient Reachability Analysis of Büchi Pushdown Systems for Hardware/Software Co-verification, J. Li, F. Xie, T. Ball, V. Levin, CAV 2010
- Towards scalable modular checking of user-defined properties, T. Ball, B. Hackett, S. K. Lahiri, S. Qadeer, J. Vanegue, VSTTE 2010
- Preemption Sealing for Efficient Concurrency Testing, T. Ball, S. Burckhardt, K. Coons, M. Musuvathi, S. Qadeer, TACAS 2010
- Chapter 23 "Evidence-Based Failure Prediction" in new book Making Software (What Really Works, and Why We Believe It), with Nachi Nagappan
- 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.
- 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
- 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!
- 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.
- Exploiting Hardware Performance Counters with Flow and Context Sensitive Profiling won the Most Influential PLDI Paper Award, PLDI 2007.
- 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
- Editorial Board, IEEE Transactions on Software Engineering
- Associate Editor, ACM Transactions on Internet Technology (2002-2006)
- Secretary/treasurer, ACM SIGPLAN (2001-2002)
- Dagstuhl Seminar on Multi-version Program Analysis
- UW/MSR 2004 Summer Institute on Trends in Testing: Theory, Techniques and Tools
- UW/MSR 2001 Summer Institute on Specifying and Checking Properties of Software
- PLDI'01 Birds-of-feather session: Specifying and Checking Properties of Software
- 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), Theoretical Computer Science
- 2010: Runtime Verification
- 2008: India Software Engineering Conference
- 2006: VMCAI'06
- 2005: PDPAR'05, SAS'05, AADEBUG'05, CAV'05, ICSE '05 Experience Reports
- 2004: SAS'04, Metrics '04, TAV-WEB '04, POPL'04
- 2003: SPIN'03
- 2002: CAV'02, PLDI'02, TACAS'02, PASTE'02 (with FSE'02)
- 2001: Workshop on Software Model Checking, SPIN'01 , ICSE'01, SAINT'01
- 2000: FSE'00, ISSTA'00, TACAS'00
- 1999: DSL'99
I grew up in Summit, NJ, where my claim to fame was writing a game for the Apple II 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".
The "Thomas Ball" Collection
Office: (425) 703-8591
Fax: (425) 936-7329
Mail: One Microsoft Way, Redmond, WA 98052