Thomas Ball

Affiliations:
  • Microsoft Research


According to our database1, Thomas Ball authored at least 126 papers between 1993 and 2023.

Collaborative distances:
  • Dijkstra number2 of two.
  • Erdős number3 of three.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2023
Symbolic Automata: ω-Regularity Modulo Theories.
CoRR, 2023

2022
Plug-and-play Physical Computing with Jacdac.
Proc. ACM Interact. Mob. Wearable Ubiquitous Technol., 2022

How families design and program games: a qualitative analysis of a 4-week online in-home study.
Proceedings of the IDC '22: Interaction Design and Children, Braga, Portugal, June 27, 2022

2021
Web-based Programming for Low-cost Gaming Handhelds.
Proceedings of the FDG'21: The 16th International Conference on the Foundations of Digital Games 2021, 2021

Rethinking the Runway: Using Avant-Garde Fashion To Design a System for Wearables.
Proceedings of the CHI '21: CHI Conference on Human Factors in Computing Systems, 2021

2020
Physical Computing: A Key Element of Modern Computer Science Education.
Computer, 2020

The BBC micro: bit: from the U.K. to the world.
Commun. ACM, 2020

TileCode: Creation of Video Games on Gaming Handhelds.
Proceedings of the UIST '20: The 33rd Annual ACM Symposium on User Interface Software and Technology, 2020

2019
MakeCode and CODAL: Intuitive and efficient embedded systems programming for education.
J. Syst. Archit., 2019

Microsoft MakeCode: embedded programming for education, in blocks and TypeScript.
Proceedings of the SPLASH-E '19, 2019

Static TypeScript: an implementation of a static compiler for the TypeScript language.
Proceedings of the 16th ACM SIGPLAN International Conference on Managed Programming Languages and Runtimes, 2019

MakerArcade: Using Gaming and Physical Computing for Playful Making, Learning, and Creativity.
Proceedings of the Extended Abstracts of the 2019 CHI Conference on Human Factors in Computing Systems, 2019

2018
Multi-platform computing for physical devices via MakeCode and CODAL.
Proceedings of the 40th International Conference on Software Engineering: Companion Proceeedings, 2018

KEYNOTE. Push, Pull, Partner: A Few Models for Working with Industry.
Proceedings of the 2018 IEEE International Conference on Software Architecture Companion, 2018

ARcadia: A Rapid Prototyping Platform for Real-time Tangible Interfaces.
Proceedings of the 2018 CHI Conference on Human Factors in Computing Systems, 2018

2017
The Micro: bit: Hands-on Computing for the New Generation (Abstract Only).
Proceedings of the 2017 ACM SIGCSE Technical Symposium on Computer Science Education, 2017

Physical computing for everyone.
Proceedings of the 39th IEEE/ACM International Conference on Software Engineering: Software Engineering Education and Training Track, 2017

2016
2014 CAV award announcement.
Formal Methods Syst. Des., 2016

CloudSDV Enabling Static Driver Verifier Using Microsoft Azure.
Proceedings of the Integrated Formal Methods - 12th International Conference, 2016

Microsoft touch develop and the BBC micro: bit.
Proceedings of the 38th International Conference on Software Engineering, 2016

2015
Deconstructing Dynamic Symbolic Execution.
Proceedings of the Dependable Software Systems Engineering, 2015

Teach foundational language principles.
Commun. ACM, 2015

Beyond Open Source: The Touch Develop Cloud-Based Integrated Development Environment.
Proceedings of the 2nd ACM International Conference on Mobile Software Engineering and Systems, 2015

2014
Efficient Tracing of Cold Code via Bias-Free Sampling.
Proceedings of the 2014 USENIX Annual Technical Conference, 2014

Correctness via compilation to logic: a decade of verification at microsoft research.
Proceedings of the 2014 ACM SIGAda annual conference on High integrity language technology, 2014

VeriCon: towards verifying controller programs in software-defined networks.
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2014

TouchDevelop: create rich mobile apps on touch devices (tutorial).
Proceedings of the 1st International Conference on Mobile Software Engineering and Systems, 2014

2013
Increasing human-tool interaction via the web.
Proceedings of the ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, 2013

Efficient modular SAT solving for IC3.
Proceedings of the Formal Methods in Computer-Aided Design, 2013

2012
Automatic predicate abstraction of C programs.
ACM SIGPLAN Notices, 2012

Beyond First-Order Satisfaction: Fixed Points, Interpolants, Automata and Polynomials.
Proceedings of the Model Checking Software - 19th International Workshop, 2012

Type-directed completion of partial expressions.
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2012

Modular and verified automatic program repair.
Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2012

2011
Predictable and Progressive Testing of Multithreaded Code.
IEEE Softw., 2011

A decade of software model checking with SLAM.
Commun. ACM, 2011

Practical parallel and concurrent programming.
Proceedings of the 42nd ACM technical symposium on Computer science education, 2011

Two for the price of one: a model for parallel and incremental computation.
Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2011

Formalizing hardware/software interface specifications.
Proceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011), 2011

Model Checking Büchi Pushdown Systems.
Proceedings of the Fundamental Approaches to Software Engineering, 2011

Evidence-Based Failure Prediction.
Proceedings of the Making Software - What Really Works, and Why We Believe It., 2011

2010
Towards Scalable Modular Checking of User-Defined Properties.
Proceedings of the Verified Software: Theories, 2010

Preemption Sealing for Efficient Concurrency Testing.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010

SLAM2: Static driver verification with under 4% false alarms.
Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, 2010

An Automata-Theoretic Approach to Hardware/Software Co-verification.
Proceedings of the Fundamental Approaches to Software Engineering, 2010

Efficient Reachability Analysis of Büchi Pushdown Systems for Hardware/Software Co-verification.
Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

The Static Driver Verifier Research Platform.
Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

2009
A brief history of software - from Bell Labs to Microsoft Research.
Proceedings of the 6th International Working Conference on Mining Software Repositories, 2009

Deconstructing concurrency heisenbugs.
Proceedings of the 31st International Conference on Software Engineering, 2009

09411 Executive Summary - Interaction versus Automation: The two Faces of Deductions.
Proceedings of the Interaction versus Automation: The two Faces of Deduction, 04.10., 2009

09411 Abstracts Collection - Interaction versus Automation: The two Faces of Deduction.
Proceedings of the Interaction versus Automation: The two Faces of Deduction, 04.10., 2009

2008
Vacuity in Testing.
Proceedings of the Tests and Proofs - 2nd International Conference, 2008

Synthesizing Monitors for Safety Properties: This Time with Calls and Returns.
Proceedings of the Runtime Verification, 8th International Workshop, 2008

Finding and Reproducing Heisenbugs in Concurrent Programs.
Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation, 2008

Finding errors in .net with feedback-directed random testing.
Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, 2008

2007
Predicate Abstraction via Symbolic Decision Procedures.
Log. Methods Comput. Sci., 2007

Better Under-Approximation of Programs by Hiding Variables.
Proceedings of the Verification, 2007

Feedback-Directed Random Test Generation.
Proceedings of the 29th International Conference on Software Engineering (ICSE 2007), 2007

Using Software Dependencies and Churn Metrics to Predict Field Failures: An Empirical Case Study.
Proceedings of the First International Symposium on Empirical Software Engineering and Measurement, 2007

Leaping Loops in the Presence of Abstraction.
Proceedings of the Computer Aided Verification, 19th International Conference, 2007

2006
Intelligent Systems and Formal Methods in Software Engineering.
IEEE Intell. Syst., 2006

An Abstraction-Refinement Framework for Multi-Agent Systems.
Proceedings of the 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 2006

Testing, abstraction, theorem proving: better together!
Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, 2006

Using Historical In-Process and Product Metrics for Early Estimation of Software Failures.
Proceedings of the 17th International Symposium on Software Reliability Engineering (ISSRE 2006), 2006

Assessing the Relationship between Software Assertions and Faults: An Empirical Investigation.
Proceedings of the 17th International Symposium on Software Reliability Engineering (ISSRE 2006), 2006

Mining metrics to predict component failures.
Proceedings of the 28th International Conference on Software Engineering (ICSE 2006), 2006

Thorough static analysis of device drivers.
Proceedings of the 2006 EuroSys Conference, Leuven, Belgium, April 18-21, 2006, 2006

Automated Abstraction of Software.
Proceedings of the Automated Technology for Verification and Analysis, 2006

2005
Polymorphic predicate abstraction.
ACM Trans. Program. Lang. Syst., 2005

The Verified Software Challenge: A Call for a Holistic Approach to Reliability.
Proceedings of the Verified Software: Theories, 2005

Zap: Automated Theorem Proving for Software Analysis.
Proceedings of the Logic for Programming, 2005

Static analysis tools as early indicators of pre-release defect density.
Proceedings of the 27th International Conference on Software Engineering (ICSE 2005), 2005

Use of relative code churn measures to predict system defect density.
Proceedings of the 27th International Conference on Software Engineering (ICSE 2005), 2005

05261 Abstracts Collection - Multi-Version Program Analysis.
Proceedings of the Multi-Version Program Analysis, 26. June - 1. July 2005, 2005

05261 Summary - Multi-Version Program Analysis.
Proceedings of the Multi-Version Program Analysis, 26. June - 1. July 2005, 2005

Abstraction for Falsification.
Proceedings of the Computer Aided Verification, 17th International Conference, 2005

2004
Righting Software.
IEEE Softw., 2004

Automatic Creation of Environment Models via Training.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004

Refining Approximations in Software Predicate Abstraction.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004

Reasoning About Systems with Transition Fairness.
Proceedings of the Logic for Programming, 2004

SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft.
Proceedings of the Integrated Formal Methods, 4th International Conference, 2004

A Theory of Predicate-Complete Test Coverage and Generation.
Proceedings of the Formal Methods for Components and Objects, 2004

Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement.
Proceedings of the Computer Aided Verification, 16th International Conference, 2004

2003
Boolean and Cartesian abstraction for model checking C programs.
Int. J. Softw. Tools Technol. Transf., 2003

From symptom to cause: localizing errors in counterexample traces.
Proceedings of the Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2003

2002
Using Version Control Data to Evaluate the Impact of Software Tools: A Case Study of the Version Editor.
IEEE Trans. Software Eng., 2002

Relative Completeness of Abstraction Refinement for Software Model Checking.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2002

Speeding Up Dataflow Analysis Using Flow-Insensitive Pointer Analysis.
Proceedings of the Static Analysis, 9th International Symposium, 2002

The SLAM project: debugging system software via static analysis.
Proceedings of the Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2002

Secrets of Software Model Checking.
Proceedings of the AGP 2002: Proceedings of the Joint Conference on Declarative Programming, 2002

2001
SIGPLANet - A Modest Proposal for SIGPLAN in the 21<sup>st</sup> Century.
ACM SIGPLAN Notices, 2001

Parameterized Verification of Multithreaded Software Libraries.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2001

Automatically Validating Temporal Safety Properties of Interfaces.
Proceedings of the Model Checking Software, 2001

Bebop: a path-sensitive interprocedural dataflow engine.
Proceedings of the 2001 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis For Software Tools and Engineering, 2001

The SLAM Toolkit.
Proceedings of the Computer Aided Verification, 13th International Conference, 2001

2000
State Generation and Automated Class Testing.
Softw. Test. Verification Reliab., 2000

Sisl: Several Interfaces, Single Logic.
Int. J. Speech Technol., 2000

Using Paths to Measure, Explain, and Enhance Program Behavior.
Computer, 2000

Speech-enabled services using TelePortal<sup>TM</sup> software and VoiceXML<sup>star</sup>.
Bell Labs Tech. J., 2000

Bebop: A Symbolic Model Checker for Boolean Programs.
Proceedings of the SPIN Model Checking and Software Verification, 7th International SPIN Workshop, Stanford, CA, USA, August 30, 2000

1999
Mawl: A Domain-Specific Language for Form-Based Services.
IEEE Trans. Software Eng., 1999

Paths between Imperative and Functional Programming.
ACM SIGPLAN Notices, 1999

Using Version Control Data to Evaluate the Impact of Software Tools.
Proceedings of the 1999 International Conference on Software Engineering, 1999

Coping with Type Casts in C.
Proceedings of the Software Engineering, 1999

The Concept of Dynamic Analysis.
Proceedings of the Software Engineering, 1999

1998
The AT&T Internet Difference Engine: Tracking and Viewing Changes on the Web.
World Wide Web, 1998

Edge Profiling versus Path Profiling: The Showdown.
Proceedings of the POPL '98, 1998

On the Limit of Control Flow Analysis for Regression Test Selection.
Proceedings of ACM SIGSOFT International Symposium on Software Testing and Analysis, 1998

1997
Integrated web and telephone service creation.
Bell Labs Tech. J., 1997

Exploiting Hardware Performance Counters with Flow and Context Sensitive Profiling.
Proceedings of the ACM SIGPLAN '97 Conference on Programming Language Design and Implementation (PLDI), 1997

Visualizing Interactions in Program Executions.
Proceedings of the Pulling Together, 1997

The Use of Program Profiling for Software Maintenance with Applications to the Year 2000 Problem.
Proceedings of the Software Engineering, 1997

Experience with a Domain Specific Language for Form-based Services.
Proceedings of the Conference on Domain-Specific Languages, 1997

1996
Software Visualization in the Large.
Computer, 1996

WebGUIDE: Querying and Navigating Changes in Web Repositories.
Comput. Networks, 1996

Tracking and Viewing Changes on the Web.
Proceedings of the USENIX Annual Technical Conference, 1996

Efficient Path Profiling.
Proceedings of the 29th Annual IEEE/ACM International Symposium on Microarchitecture, 1996

An Internet Difference Engine and its Applications.
Proceedings of the Forty-First IEEE Computer Society International Conference: Technologies for the Information Superhighway, 1996

1995
Storm Watch: A Tool for Visualizing Memory System Protocols.
Proceedings of the Proceedings Supercomputing '95, San Diego, CA, USA, December 4-8, 1995, 1995

1994
Optimally Profiling and Tracing Programs.
ACM Trans. Program. Lang. Syst., 1994

Efficient Counting Program Events with Support for On-Line Queries.
ACM Trans. Program. Lang. Syst., 1994

Rewriting Executable Files to Measure Program Behavior.
Softw. Pract. Exp., 1994

Visualizing Program Slices.
Proceedings of the Proceedings IEEE Symposium on Visual Languages, 1994

End-to-end Service Survivability- Study Methodology Root Cause Analysis Solution Alternatives.
Proceedings of NOMS '94, 1994

1993
What's In a Region? Or Computing Control Dependence Regions In Near-Linear Time for Reducible Control Flow.
LOPLAS, 1993

Branch Prediction For Free.
Proceedings of the ACM SIGPLAN'93 Conference on Programming Language Design and Implementation (PLDI), 1993

Slicing Programs with Arbitrary Control-flow.
Proceedings of the Automated and Algorithmic Debugging, First International Workshop, 1993


  Loading...