Author image not provided
 Thomas Jaudon Ball

Add personal information
  Affiliation history
Bibliometrics: publication history
Average citations per article46.94
Citation Count4,412
Publication count94
Publication years1979-2016
Available for download45
Average downloads per article1,325.44
Downloads (cumulative)59,645
Downloads (12 Months)3,323
Downloads (6 Weeks)308
ACM Fellow
Arrow RightAuthor only
· Editor only
· Other only
· All roles

See all colleagues of this author

See all subject areas

See all author supplied keywords

Project background Author-Izer logoAuthor-Izer Service


95 results found Export Results: bibtex | endnote | acmref | csv

Result 1 – 20 of 95
Result page: 1 2 3 4 5

Sort by:

1 published by ACM
March 2017 SIGCSE '17: Proceedings of the 2017 ACM SIGCSE Technical Symposium on Computer Science Education
Publisher: ACM
Citation Count: 0

The micro:bit ( is a pocket-sized, programmable computing device, designed to engage people with computing technology. The micro:bit is visually appealing, fun, easy to code and inexpensive. It is widely available at schools in the United Kingdom and is now being rolled out world-wide. Key features of the micro:bit that ...
Keywords: safe javascript, micro:bit, K-12, browser based programming, physical computing

2014 CAV award announcement
June 2016 Formal Methods in System Design: Volume 48 Issue 3, June 2016
Publisher: Kluwer Academic Publishers
Citation Count: 0

The 2014 computer-aided verification (CAV) award was presented on July 19, 2014, at the 26th annual CAV conference in Vienna to Patrice Godefroid, Doron Peled, Antti Valmari, and Pierre Wolper for the development of partial-order-reduction algorithms for efficient state-space exploration of concurrent systems.
Keywords: Concurrency, CAV Award, Computer-aided verification, Model checking, Partial order reduction

CloudSDV Enabling Static Driver Verifier Using Microsoft Azure
Rahul Kumar, Thomas Ball, Jakob Lichtenberg, Nate Deisinger, Apoorv Upreti, Chetan Bansal
June 2016 IFM 2016: Proceedings of the 12th International Conference on Integrated Formal Methods - Volume 9681
Publisher: Springer-Verlag New York, Inc.
Citation Count: 0

In this paper we describe our experience of enabling Static Driver Verifier to use the Microsoft Azure cloud computing platform. We first describe in detail our architecture and methodology for enabling SDV to operate in the Microsoft Azure cloud. We then present our results of using CloudSDV on single drivers ...
Keywords: Azure, SDV, Verification, Cloud, Performance, Scalability, Static analysis, Parallel

4 published by ACM
May 2016 ICSE '16: Proceedings of the 38th International Conference on Software Engineering Companion
Publisher: ACM
Citation Count: 1
Downloads (6 Weeks): 4,   Downloads (12 Months): 65,   Downloads (Overall): 92

Full text available: PDFPDF
The chance to influence the lives of a million children does not come often. Through a partnership between the BBC and several technology companies, a small instructional computing device called the BBC micro:bit will be given to a million children in the UK in 2016. Moreover, using the micro:bit will ...
Keywords: K-12 education, devices, BBC micro:bit, cloud, touch develop

Beyond Open Source: The Touch Develop Cloud-Based Integrated Development Environment
May 2015 MOBILESOFT '15: Proceedings of the 2015 2nd ACM International Conference on Mobile Software Engineering and Systems
Publisher: IEEE Computer Society
Citation Count: 0

Software engineering tools and environments are migrating to the cloud, enabling more people to participate in programming from many more devices. To study this phenomenon in detail, we designed, implemented and deployed Touch Develop (url, a cloud-based integrated development environment (CIDE), which has been online for the past three ...

Beyond open source: the TouchDevelop cloud-based integrated development environment
May 2015 MOBILESoft '15: Proceedings of the Second ACM International Conference on Mobile Software Engineering and Systems
Publisher: IEEE Press
Citation Count: 2
Downloads (6 Weeks): 3,   Downloads (12 Months): 17,   Downloads (Overall): 31

Full text available: PDFPDF
Software engineering tools and environments are migrating to the cloud, enabling more people to participate in programming from many more devices. To study this phenomenon in detail, we designed, implemented and deployed TouchDevelop (, a cloud-based integrated development environment (CIDE), which has been online for the past three years. TouchDevelop ...

7 published by ACM
Teach foundational language principles
April 2015 Communications of the ACM: Volume 58 Issue 5, May 2015
Publisher: ACM
Citation Count: 0
Downloads (6 Weeks): 12,   Downloads (12 Months): 237,   Downloads (Overall): 12,235

Full text available: HtmlHtml  PDFPDF  PDF Chinese translationPDF Chinese translation
Industry is ready and waiting for more graduates educated in the principles of programming languages.

8 published by ACM
Correctness via compilation to logic: a decade of verification at microsoft research
October 2014 HILT '14: Proceedings of the 2014 ACM SIGAda annual conference on High integrity language technology
Publisher: ACM
Citation Count: 0
Downloads (6 Weeks): 1,   Downloads (12 Months): 13,   Downloads (Overall): 57

Full text available: PDFPDF
Advances in automated theorem provers over the last decade have led to a renaissance in software tools that compile problems of correctness to problems over logic formula. In this talk, I will review progress in automated theorem provers, such as Z3 from Microsoft Research, and consider a variety of program ...
Keywords: program verification, interactive functional verification, automated theorem proving, program testing
Also published in:
November 2014  ACM SIGAda Ada Letters - HILT '14: Volume 34 Issue 3, December 2014

Efficient tracing of cold code via bias-free sampling
Baris Kasikci, Thomas Ball, George Candea, John Erickson, Madanlal Musuvathi
June 2014 USENIX ATC'14: Proceedings of the 2014 USENIX conference on USENIX Annual Technical Conference
Publisher: USENIX Association
Citation Count: 3

Bugs often lurk in code that is infrequently executed (i.e., cold code), so testing and debugging requires tracing such code. Alas, the location of cold code is generally not known a priori and, by definition, cold code is elusive during execution. Thus, programs either incur unnecessary runtime overhead to "catch" ...

10 published by ACM
VeriCon: towards verifying controller programs in software-defined networks
Thomas Ball, Nikolaj Bjørner, Aaron Gember, Shachar Itzhaky, Aleksandr Karbyshev, Mooly Sagiv, Michael Schapira, Asaf Valadarsky
June 2014 PLDI '14: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation
Publisher: ACM
Citation Count: 24
Downloads (6 Weeks): 11,   Downloads (12 Months): 111,   Downloads (Overall): 602

Full text available: PDFPDF
Software-defined networking (SDN) is a new paradigm for operating and managing computer networks. SDN enables logically-centralized control over network devices through a "controller" software that operates independently from the network hardware, and can be viewed as the network operating system. Network operators can run both inhouse and third-party SDN programs ...
Keywords: software-defined networks, Hoare-style verification
Also published in:
June 2014  ACM SIGPLAN Notices - PLDI '14: Volume 49 Issue 6, June 2014

11 published by ACM
TouchDevelop: create rich mobile apps on touch devices (tutorial)
June 2014 MOBILESoft 2014: Proceedings of the 1st International Conference on Mobile Software Engineering and Systems
Publisher: ACM
Citation Count: 0
Downloads (6 Weeks): 1,   Downloads (12 Months): 9,   Downloads (Overall): 87

Full text available: PDFPDF
We are experiencing a technology shift: Powerful and easy-to-use mobile devices like smartphones and tablets are becoming more prevalent than traditional PCs and laptops. Mobile devices are going to be the first and, in less developed countries, possibly the only computing devices which virtually all people will own and carry ...
Keywords: touch-based entry, Web IDE, tablet, mobile devices, smart phone

12 published by ACM
Increasing human-tool interaction via the web
Thomas Ball, Peli de Halleux, Nikhil Swamy, Daan Leijen
June 2013 PASTE '13: Proceedings of the 11th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering
Publisher: ACM
Citation Count: 0
Downloads (6 Weeks): 1,   Downloads (12 Months): 15,   Downloads (Overall): 62

Full text available: PDFPDF
Software tools researchers can accelerate their ability to learn by exposing tools to users via web technologies, allowing them to observe and test the interactions between humans and tools. At Microsoft Research, we have developed a web service ( for such a purpose that is available for community use.
Keywords: web services, software tools

13 published by ACM
Type-directed completion of partial expressions
June 2012 PLDI '12: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation
Publisher: ACM
Citation Count: 26
Downloads (6 Weeks): 3,   Downloads (12 Months): 31,   Downloads (Overall): 349

Full text available: PDFPDF
Modern programming frameworks provide enormous libraries arranged in complex structures, so much so that a large part of modern programming is searching for APIs that surely exist" somewhere in an unfamiliar part of the framework. We present a novel way of phrasing a search for an unknown API: the programmer ...
Keywords: program synthesis, type-based analysis, partial expressions, ranking, code completion
Also published in:
August 2012  ACM SIGPLAN Notices - PLDI '12: Volume 47 Issue 6, June 2012

Formalizing hardware/software interface specifications
Juncao Li, Fei Xie, Thomas Ball, Vladimir Levin, Con McGarvey
November 2011 ASE '11: Proceedings of the 2011 26th IEEE/ACM International Conference on Automated Software Engineering
Publisher: IEEE Computer Society
Citation Count: 3
Downloads (6 Weeks): 2,   Downloads (12 Months): 19,   Downloads (Overall): 119

Full text available: PDFPDF
Software drivers are usually developed after hardware devices become available. This dependency can induce a long product cycle. Although co-simulation and co-verification techniques have been utilized to facilitate the driver development, Hardware/Software (HW/SW) interface models, as the test harnesses, are often challenging to specify. Such interface models should have formal ...

15 published by ACM
Two for the price of one: a model for parallel and incremental computation
Sebastian Burckhardt, Daan Leijen, Caitlin Sadowski, Jaeheon Yi, Thomas Ball
October 2011 OOPSLA '11: Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications
Publisher: ACM
Citation Count: 16
Downloads (6 Weeks): 3,   Downloads (12 Months): 22,   Downloads (Overall): 389

Full text available: PDFPDF
Parallel or incremental versions of an algorithm can significantly outperform their counterparts, but are often difficult to develop. Programming models that provide appropriate abstractions to decompose data and tasks can simplify parallelization. We show in this work that the same abstractions can enable both parallel and incremental execution. We present ...
Keywords: self-adjusting computation, incremental memoization, parallel programming
Also published in:
October 2011  ACM SIGPLAN Notices - OOPSLA '11: Volume 46 Issue 10, October 2011

16 published by ACM
A decade of software model checking with SLAM
Thomas Ball, Vladimir Levin, Sriram K. Rajamani
July 2011 Communications of the ACM: Volume 54 Issue 7, July 2011
Publisher: ACM
Citation Count: 50
Downloads (6 Weeks): 72,   Downloads (12 Months): 1,062,   Downloads (Overall): 8,850

Full text available: HtmlHtml  PDFPDF
SLAM is a program-analysis engine used to check if clients of an API follow the API's stateful usage rules.

Predictable and Progressive Testing of Multithreaded Code
May 2011 IEEE Software: Volume 28 Issue 3, May 2011
Publisher: IEEE Computer Society Press
Citation Count: 1

Developing concurrent software is hard. Testing concurrent software is harder. Although sequential program testing has many useful concepts, techniques, and tools (for example, assertions, unit testing, test-driven development, code coverage, and test generation tools), the testing workbench for concurrent programs is comparatively quite bare. Chess is a new testing tool ...
Keywords: Chess, sequential program, concurrency, threads scheduling, testing, nondeterminism, software

Model checking büchi pushdown systems
Juncao Li, Fei Xie, Thomas Ball, Vladimir Levin
March 2011 FASE'11/ETAPS'11: Proceedings of the 14th international conference on Fundamental approaches to software engineering: part of the joint European conferences on theory and practice of software
Publisher: Springer-Verlag
Citation Count: 1

We develop an approach to model checking Linear Temporal Logic (LTL) properties of Büchi Pushdown Systems (BPDS). Such BPDS models are suitable for Hardware/Software (HW/SW) co-verification. Since a BPDS represents the asynchronous transitions between hardware and software, some transition orders are unnecessary to be explored in verification. We design an ...

19 published by ACM
Practical parallel and concurrent programming
Caitlin Sadowski, Thomas Ball, Judith Bishop, Sebastian Burckhardt, Ganesh Gopalakrishnan, Joseph Mayo, Madanlal Musuvathi, Shaz Qadeer, Stephen Toub
March 2011 SIGCSE '11: Proceedings of the 42nd ACM technical symposium on Computer science education
Publisher: ACM
Citation Count: 6
Downloads (6 Weeks): 3,   Downloads (12 Months): 19,   Downloads (Overall): 369

Full text available: PDFPDF
Multicore computers are now the norm. Taking advantage of these multiple cores entails parallel and concurrent programming. There is therefore a pressing need for courses that teach effective programming on multicore architectures. We believe that such courses should emphasize high-level abstractions for performance and correctness and be supported by tools. ...
Keywords: distributed, multicore, parallelism, tools, concurrency

SLAM2: static driver verification with under 4% false alarms
Thomas Ball, Ella Bounimova, Rahul Kumar, Vladimir Levin
October 2010 FMCAD '10: Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design
Publisher: FMCAD Inc
Citation Count: 20
Downloads (6 Weeks): 3,   Downloads (12 Months): 19,   Downloads (Overall): 74

Full text available: PDFPDF
In theory, counterexample-guided abstraction refinement (CEGAR) uses spurious counterexamples to refine overapproximations so as to eliminate provably false alarms. In practice, CEGAR can report false alarms because: (1) the underlying problem CEGAR is trying to solve is undecidable; (2) approximations introduced for optimization purposes may cause CEGAR to be unable ...

The ACM Digital Library is published by the Association for Computing Machinery. Copyright © 2017 ACM, Inc.
Terms of Usage   Privacy Policy   Code of Ethics   Contact Us