Thomas Ball - Papers

2008

• Finding and Reproducing Heisenbugs in Concurrent Programs, M. Musuvathi, S. Qadeer, T. Ball, G. Basler, P. A. Nainar, I. Neamtiu, To Appear, OSDI 2008
• Finding Errors in .NET with Feedback-Directed Random Testing, Carlos Pacheco, Shuvendu Lahiri, Thomas Ball. MSR-TR-2008-29, February 2008. ISSTA 2008
• First-class Concurrency Debugging and Testing. S. Burckhardt, T. Ball, M. Musuvathi, and S. Qadeer. Position paper, Workshop on Exploiting Concurrency Efficiently and Correctly, 2008.
• CHESS: A Systematic Testing Tool for Concurrent Software. M. Musuvathi, S. Qadeer, and T. Ball. Microsoft Research Technical Report MSR-TR-2007-149, 2007.
• Annotation-based property checking for systems software, T. Ball, B. Hackett, S. Lahiri, and S. Qadeer. Microsoft Research Technical Report MSR-TR-2008-82, May 2008
• Vacuity in Testing, Thomas Ball, Orna Kupferman. Second International Conference of Tests and Proofs.
• Synthesizing Monitors for Safety Properties - This Time With Calls and Returns, Grigore Rosu, Feng Chen, Thomas Ball. Run-time Verification Workshop 2008

2007

• Better Under-approximation of Programs by Hiding Variables, Thomas Ball, Orna Kupferman, VMCAI 2007
• Feedback-directed Random Test Generation, Carlos Pacheco, Shuvendu Lahiri, Michael Ernst, Thomas Ball. ICSE 2007
• Leaping Loops in the Presence of Abstraction, Thomas Ball, Orna Kupferman, Mooly Sagiv:  CAV 2007: 491-503.

• Using Software Dependencies and Churn Metrics to Predict Field Failures: An Empirical Case Study, Nagappan, N., Ball, T. Proceedings of the Empirical Software Engineering and Measurement Conference (ESEM), Madrid, Spain 2007.

2006

• Intelligent Systems and Formal Methods in Software Engineering, Bernhard Beckert, Tony Hoare, Reiner Hähnle, Douglas R. Smith, Cordell Green, Silvio Ranise, Cesare Tinelli, Thomas Ball, Sriram K. Rajamani, IEEE Intelligent Systems, November/December 2006 (Vol. 21, No. 6)
• An Abstraction-Refinement Framework for Multi-Agent Systems, Thomas Ball and Orna Kupferman, LICS 2006 , August 2006
• Testing, Abstraction, Theorem Proving: Better Together, Greta Yorsh, Thomas Ball, Mooly Sagiv, ISSTA 2006
• Mining metrics to predict component failures [MSR TR] Nachiappan Nagappan, Thomas Ball, Andreas Zeller, International Conference on Software Engineering, Shanghai, China, May 2006.
• Assessing the Relationship between Software Assertions and Code Quality:An Empirical Investigation, Gunnar Kudrjavets, Nachiappan Nagappan, Thomas Ball. MSR-TR-2006-54, May 2006.
• Thorough Static Analysis of Device Drivers, Thomas Ball, Ella Bounimova, Byron Cook, Vladimir Levin, Jakob Lichtenberg, Con McGarvey, Bohus Ondrusek, Sriram K. Rajamani and Abdullah Ustuner (Microsoft), EuroSys 2006, April 2006.
• Explaining Failures Using Software Dependences and Churn Metrics, Nachiappan Nagappan, Thomas Ball. MSR-TR-2006-03, January 2006.

2005

• The Verified Software Challenge: A Call for a Holistic Approach to Reliability, Thomas Ball, Verified Software: Theories, Tools, Experiments Conference
• Zap: Automated Theorem Proving for Software Analysis,Thomas Ball, Shuvendu K. Lahiri, Madanlal Musuvathi. LPAR 2005: 2-22
• Abstraction for Falsification, Thomas Ball, Orna Kupferman, Greta Yorsh. CAV 2005: 67-81
• Predicate Abstraction via Symbolic Decision Procedures. Shuvendu K. Lahiri, Thomas Ball, Byron Cook. CAV 2005: 24-38
• Use of relative code churn measures to predict system defect density. Nachiappan Nagappan, Thomas Ball. ICSE 2005: 284-292
• Static analysis tools as early indicators of pre-release defect density, Nachiappan Nagappan, Thomas Ball. ICSE 2005: 580-586
• Polymorphic predicate abstraction, Thomas Ball, Todd D. Millstein, Sriram K. Rajamani. ACM Trans. Program. Lang. Syst. 27(2): 314-343 (2005)

2004

• Formalizing Counterexample-driven Refinement with Weakest Preconditions, Thomas Ball, MSR-TR-2004-134, proceedings of 2004 Marktoberdorf Summer School
• Reasoning About Systems with Transition Fairness: Benjamin Aminof, Thomas Ball, Orna Kupferman. LPAR 2004: 194-208
• Righting Software, James R. Larus, Thomas Ball, Manuvir Das, Robert DeLine, Manuel Fähndrich, Jonathan D. Pincus, Sriram K. Rajamani, Ramanathan Venkatapathy. IEEE Software 21(3): 92-100 (2004)
• A Theory of Predicate-Complete Test Coverage and Generation, Thomas Ball. FMCO 2004: 1-22
• SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft, Thomas Ball, Byron Cook, Vladimir Levin, Sriram K. Rajamani. IFM 2004: 1-20
• Automatic Creation of Environment Models via Training, Thomas Ball, Vladimir Levin, Fei Xie. TACAS 2004: 93-107
• Refining Approximations in Software Predicate Abstraction, Thomas Ball, Byron Cook, Satyaki Das, Sriram K. Rajamani. TACAS 2004: 388-403

2003

• Abstraction-guided Test Generation: A Case Study, Thomas Ball. MSR-TR-2003-86, November 2003.
• Boolean and Cartesian abstraction for model checking C programs, Thomas Ball, Andreas Podelski, Sriram K. Rajamani. STTT 5(1): 49-58 (2003)
• From symptom to cause: localizing errors in counterexample traces, Thomas Ball, Mayur Naik, Sriram K. Rajamani. POPL 2003: 97-105

2002

• Speeding Up Dataflow Analysis Using Flow-Insensitive Pointer Analysis, Stephen Adams, Thomas Ball, Manuvir Das, Sorin Lerner, Sriram K. Rajamani, Mark Seigle, Westley Weimer. SAS 2002: 230-246
• Using Version Control Data to Evaluate the Impact of Software Tools: A Case Study of the Version Editor, David L. Atkins, Thomas Ball, Todd L. Graves, Audris Mockus. IEEE Trans. Software Eng. 28(7): 625-637 (2002)
• Relative Completeness of Abstraction Refinement for Software Model Checking, Thomas Ball, Andreas Podelski, Sriram K. Rajamani. TACAS 2002: 158-172
• The SLAM project: debugging system software via static analysis, Thomas Ball, Sriram K. Rajamani. POPL 2002: 1-3

2001

• Automatic Predicate Abstraction of C Programs, Thomas Ball, Rupak Majumdar, Todd D. Millstein, Sriram K. Rajamani. PLDI 2001: 203-213
• Bebop: a path-sensitive interprocedural dataflow engine, Thomas Ball, Sriram K. Rajamani. PASTE 2001: 97-103
• The SLAM Toolkit, Thomas Ball, Sriram K. Rajamani. CAV 2001: 260-264
• Automatically Validating Temporal Safety Properties of Interfaces, Thomas Ball, Sriram K. Rajamani. SPIN 2001: 103-122
• Thomas Ball, Sagar Chaki, Sriram K. Rajamani: Parameterized Verification of Multithreaded Software Libraries. TACAS 2001: 158-173
• Boolean and Cartesian Abstraction for Model Checking C Programs, Thomas Ball, Andreas Podelski, Sriram K. Rajamani. TACAS 2001: 268-283

2000

• Thomas Ball, Daniel Hoffman, Frank Ruskey, Richard Webber, Lee J. White: State Generation and Automated Class Testing. Softw. Test., Verif. Reliab. 10(3): 149-170 (2000)
• Bebop: A Symbolic Model Checker for Boolean Programs, Thomas Ball, Sriram K. Rajamani. SPIN 2000: 113-130
• Speech-enabled services using TelePortal^TM software and VoiceXML, Thomas Ball, Veta Bonnewell, Peter J. Danielsen, Peter Mataga, Kenneth Rehor. Bell Labs Technical Journal 5(3): 98-111 (2000)
• Checking Temporal Properties of Software with Boolean Programs [ PS, PDF ], Thomas Ball, Sriram K. Rajamani, Workshop on Advances in Verification (with CAV 2000), July 2000.
• Using Paths to Measure, Explain, and Enhance Program Behavior, Thomas Ball, James R. Larus. IEEE Computer 33(7): 57-65 (2000)
• SISL: Several Interfaces, Single Logic, T. Ball, C. Colby, P. Danielsen, L. Jagadeesan, R. Jagadeesan, K. Laufer, P. Mataga, K. Rehor, International Journal of Speech Technology, Kluwer Academic Publishers, Vol. 3, No. 2, June 2000, pp 93-108
• Boolean Programs: A Model and Process for Software Analysis, T. Ball, S.K. Rajamani, MSR Technical Report 2000-14, February 2000.

1999

• Reverse engineering the Twelve Days of Christmas, Thomas Ball.
• The Concept of Dynamic Analysis, Thomas Ball. ESEC / SIGSOFT FSE 1999: 216-234
• Coping with Type Casts in C, Michael Siff, Satish Chandra, Thomas Ball, Krishna Kunchithapadam, Thomas W. Reps. ESEC / SIGSOFT FSE 1999: 180-198
• Mawl: A Domain-Specific Language for Form-Based Services, David L. Atkins, Thomas Ball, Glenn Bruns, Kenneth C. Cox. IEEE Trans. Software Eng. 25(3): 334-346 (1999)
• Using Version Control Data to Evaluate the Impact of Software Tools, David L. Atkins, Thomas Ball, Todd L. Graves, Audris Mockus. ICSE 1999: 324-333
• Paths between Imperative and Functional Programming, Thomas Ball. SIGPLAN Notices 34(2): 21-25 (1999)

1998

• Analyzing path profiles with the Hot Path Browser, T. Ball, J. R. Larus, G. Rosay, Workshop on Profile and Feedback-directed Compilation (with PACT'98), October.
• On the Limit of Control Flow Analysis for Regression Test Selection, Thomas Ball. ISSTA 1998: 134-142
• Edge Profiling versus Path Profiling: The Showdown, Thomas Ball, Peter Mataga, Shmuel Sagiv. POPL 1998: 134-148
• The AT&T Internet Difference Engine: Tracking and Viewing Changes on the Web, Fred Douglis, Thomas Ball, Yih-Farn Chen, Eleftherios Koutsofios. World Wide Web 1(1): 27-44 (1998)

1997

• Experience with a domain specific language for form-based services. D. Atkins. T. Ball, et al., Usenix Conference on Domain Specific Languages, October 1997, Santa Barbara, CA.
• The Use of Program Profiling for Software Maintenance with Applications to the Year 2000 Problem, Thomas W. Reps, Thomas Ball, Manuvir Das, James R. Larus. ESEC / SIGSOFT FSE 1997: 432-449
• Exploiting Hardware Performance Counters with Flow and Context Sensitive Profiling, Glenn Ammons, Thomas Ball, James R. Larus. PLDI 1997: 85-96
• Visualizing Interactions in Program Executions, Dean F. Jerding, John T. Stasko, Thomas Ball. ICSE 1997: 360-370
• If your version control system could talk ..., T. Ball, J.-M. Kim, A. A. Porter, H. P. Siy, ICSE '97 Workshop on Process Modelling and Empirical Studies of Software Engineering.
• Integrated web and telephone service creation, D. Atkins, T. Ball, et al., Bell Labs Technical Journal, Vol. 2, No. 1, Winter 1997.

1996

• An Internet Difference Engine and its Applications, Thomas Ball, Fred Douglis. COMPCON 1996: 71-76
• Thomas Ball, James R. Larus: Efficient Path Profiling. MICRO 1996: 46-57
• Tracking and Viewing Changes on the Web, Fred Douglis, Thomas Ball. USENIX Annual Technical Conference 1996: 165-176
• WebGUIDE: Querying and Navigating Changes in Web Repositories, Fred Douglis, Thomas Ball, Yih-Farn Chen, Eleftherios Koutsofios. Computer Networks 28(7-11): 1335-1344 (1996)
• Software Visualization in the Large. Thomas Ball, Stephen G. Eick. IEEE Computer 29(4): 33-43 (1996)

1995

• Storm Watch: A Tool for Visualizing Memory System Protocols, Trishul M. Chilimbi, Thomas Ball, Stephen G. Eick, James R. Larus. Supercomputing 1995, article #38.

1994

• Thomas Ball, Stephen G. Eick: Visualizing Program Slices. VL 1994: 288-295
• Efficient Counting Program Events with Support for On-Line Queries, Thomas Ball. ACM Trans. Program. Lang. Syst. 16(5): 1399-1410 (1994)
• Optimally Profiling and Tracing Programs, Thomas Ball, James R. Larus. ACM Trans. Program. Lang. Syst. 16(4): 1319-1360 (1994)
• Rewriting Executable Files to Measure Program Behavior, James R. Larus, Thomas Ball. Softw., Pract. Exper. 24(2): 197-218 (1994)

1993

• What's In a Region? Or Computing Control Dependence Regions In Near-Linear Time for Reducible Control Flow, Thomas Ball. LOPLAS 2(1-4): 1-16 (1993)
• Branch Prediction For Free, Thomas Ball. James R. Larus. PLDI 1993: 300-313
• Slicing Programs with Arbitrary Control-flow, Thomas Ball, Susan Horwitz. AADEBUG 1993: 206-222

1992

• Thomas Ball, James R. Larus: Optimally Profiling and Tracing Programs. POPL 1992: 59-70