Thomas Ball

Shuo Chen

Cormac Herley

CoRR, 2024

MicroData: live visualisation & recording of micro: bit sensor data.

[BibT_eX]

[DOI]

Proceedings of the 19th WiPSCE Conference on Primary and Secondary Computing Education Research, 2024

MicroCode: live, portable programming for children via robotics.

[BibT_eX]

[DOI]

Proceedings of the Adjunct Proceedings of the 37th Annual ACM Symposium on User Interface Software and Technology, 2024

Meet MicroCode: a Live and Portable Programming Tool for the BBC micro: bit.

[BibT_eX]

[DOI]

Proceedings of the 23rd Annual ACM Interaction Design and Children Conference, 2024

Imagining Inclusive Digital Maker Futures with the BBC micro: bit.

[BibT_eX]

[DOI]

Proceedings of the 23rd Annual ACM Interaction Design and Children Conference, 2024

2023

Symbolic Automata: ω-Regularity Modulo Theories.

[BibT_eX]

[DOI]

CoRR, 2023

2022

Plug-and-play Physical Computing with Jacdac.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Stefania Druga

Amy J. Ko

Proceedings of the IDC '22: Interaction Design and Children, Braga, Portugal, June 27, 2022

2021

Web-based Programming for Low-cost Gaming Handhelds.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Computer, 2020

The BBC micro: bit: from the U.K. to the world.

[BibT_eX]

[DOI]

Commun. ACM, 2020

TileCode: Creation of Video Games on Gaming Handhelds.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

J. Syst. Archit., 2019

Microsoft MakeCode: embedded programming for education, in blocks and TypeScript.

[BibT_eX]

[DOI]

Proceedings of the SPLASH-E '19, 2019

Static TypeScript: an implementation of a static compiler for the TypeScript language.

[BibT_eX]

[DOI]

Peli de Halleux

Michal Moskal

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.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Judith Bishop

Joe Finney

Proceedings of the 40th International Conference on Software Engineering: Companion Proceeedings, 2018

KEYNOTE. Push, Pull, Partner: A Few Models for Working with Industry.

[BibT_eX]

[DOI]

Proceedings of the 2018 IEEE International Conference on Software Architecture Companion, 2018

ARcadia: A Rapid Prototyping Platform for Real-time Tangible Interfaces.

[BibT_eX]

[DOI]

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).

[BibT_eX]

[DOI]

Judith Bishop

Jonathan de Halleux

Proceedings of the 2017 ACM SIGCSE Technical Symposium on Computer Science Education, 2017

Physical computing for everyone.

[BibT_eX]

[DOI]

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

2016

2014 CAV award announcement.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2016

CloudSDV Enabling Static Driver Verifier Using Microsoft Azure.

[BibT_eX]

[DOI]

Proceedings of the Integrated Formal Methods - 12th International Conference, 2016

Microsoft touch develop and the BBC micro: bit.

[BibT_eX]

[DOI]

Proceedings of the 38th International Conference on Software Engineering, 2016

2015

Deconstructing Dynamic Symbolic Execution.

[BibT_eX]

[DOI]

Jakub Daniel

Proceedings of the Dependable Software Systems Engineering, 2015

Teach foundational language principles.

[BibT_eX]

[DOI]

Benjamin G. Zorn

Commun. ACM, 2015

Beyond Open Source: The Touch Develop Cloud-Based Integrated Development Environment.

[BibT_eX]

[DOI]

Proceedings of the 2nd ACM International Conference on Mobile Software Engineering and Systems, 2015

2014

Efficient Tracing of Cold Code via Bias-Free Sampling.

[BibT_eX]

[DOI]

Proceedings of the 2014 USENIX Annual Technical Conference, 2014

Correctness via compilation to logic: a decade of verification at microsoft research.

[BibT_eX]

[DOI]

Proceedings of the 2014 ACM SIGAda annual conference on High integrity language technology, 2014

VeriCon: towards verifying controller programs in software-defined networks.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2014

TouchDevelop: create rich mobile apps on touch devices (tutorial).

[BibT_eX]

[DOI]

Proceedings of the 1st International Conference on Mobile Software Engineering and Systems, 2014

2013

Increasing human-tool interaction via the web.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, 2013

Efficient modular SAT solving for IC3.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2013

2012

Automatic predicate abstraction of C programs.

[BibT_eX]

[DOI]

ACM SIGPLAN Notices, 2012

Beyond First-Order Satisfaction: Fixed Points, Interpolants, Automata and Polynomials.

[BibT_eX]

[DOI]

Leonardo Mendonça de Moura

Nikolaj S. Bjørner

Kenneth L. McMillan

Margus Veanes

Proceedings of the Model Checking Software - 19th International Workshop, 2012

Type-directed completion of partial expressions.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2012

Modular and verified automatic program repair.

[BibT_eX]

[DOI]

Francesco Logozzo

Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2012

2011

Predictable and Progressive Testing of Multithreaded Code.

[BibT_eX]

[DOI]

IEEE Softw., 2011

A decade of software model checking with SLAM.

[BibT_eX]

[DOI]

Vladimir Levin

Commun. ACM, 2011

Practical parallel and concurrent programming.

[BibT_eX]

[DOI]

Ganesh Gopalakrishnan

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.

[BibT_eX]

[DOI]

Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2011

Formalizing hardware/software interface specifications.

[BibT_eX]

[DOI]

Proceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011), 2011

Model Checking Büchi Pushdown Systems.

[BibT_eX]

[DOI]

Proceedings of the Fundamental Approaches to Software Engineering, 2011

Evidence-Based Failure Prediction.

[BibT_eX]

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

2010

Towards Scalable Modular Checking of User-Defined Properties.

[BibT_eX]

[DOI]

Proceedings of the Verified Software: Theories, 2010

Preemption Sealing for Efficient Concurrency Testing.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010

SLAM2: Static driver verification with under 4% false alarms.

[BibT_eX]

[DOI]

Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, 2010

An Automata-Theoretic Approach to Hardware/Software Co-verification.

[BibT_eX]

[DOI]

Proceedings of the Fundamental Approaches to Software Engineering, 2010

Efficient Reachability Analysis of Büchi Pushdown Systems for Hardware/Software Co-verification.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

The Static Driver Verifier Research Platform.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

2009

A brief history of software - from Bell Labs to Microsoft Research.

[BibT_eX]

[DOI]

Proceedings of the 6th International Working Conference on Mining Software Repositories, 2009

Deconstructing concurrency heisenbugs.

[BibT_eX]

[DOI]

Proceedings of the 31st International Conference on Software Engineering, 2009

09411 Executive Summary - Interaction versus Automation: The two Faces of Deductions.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the Interaction versus Automation: The two Faces of Deduction, 04.10., 2009

2008

Vacuity in Testing.

[BibT_eX]

[DOI]

Proceedings of the Tests and Proofs - 2nd International Conference, 2008

Synthesizing Monitors for Safety Properties: This Time with Calls and Returns.

[BibT_eX]

[DOI]

Grigore Rosu

Feng Chen

Piramanayagam Arumuga Nainar

Proceedings of the Runtime Verification, 8th International Workshop, 2008

Finding and Reproducing Heisenbugs in Concurrent Programs.

[BibT_eX]

[DOI]

Iulian Neamtiu

Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation, 2008

Finding errors in .net with feedback-directed random testing.

[BibT_eX]

[DOI]

Carlos Pacheco

Shuvendu K. Lahiri

Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, 2008

2007

Predicate Abstraction via Symbolic Decision Procedures.

[BibT_eX]

[DOI]

Shuvendu K. Lahiri

Byron Cook

Log. Methods Comput. Sci., 2007

Better Under-Approximation of Programs by Hiding Variables.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2007

Feedback-Directed Random Test Generation.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the First International Symposium on Empirical Software Engineering and Measurement, 2007

Leaping Loops in the Presence of Abstraction.

[BibT_eX]

[DOI]

Mooly Sagiv

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

2006

Intelligent Systems and Formal Methods in Software Engineering.

[BibT_eX]

[DOI]

IEEE Intell. Syst., 2006

An Abstraction-Refinement Framework for Multi-Agent Systems.

[BibT_eX]

[DOI]

Proceedings of the 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 2006

Testing, abstraction, theorem proving: better together!

[BibT_eX]

[DOI]

Greta Yorsh

Mooly Sagiv

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.

[BibT_eX]

[DOI]

Brendan Murphy

Proceedings of the 17th International Symposium on Software Reliability Engineering (ISSRE 2006), 2006

Assessing the Relationship between Software Assertions and Faults: An Empirical Investigation.

[BibT_eX]

[DOI]

Gunnar Kudrjavets

Proceedings of the 17th International Symposium on Software Reliability Engineering (ISSRE 2006), 2006

Mining metrics to predict component failures.

[BibT_eX]

[DOI]

Andreas Zeller

Proceedings of the 28th International Conference on Software Engineering (ICSE 2006), 2006

Thorough static analysis of device drivers.

[BibT_eX]

[DOI]

Proceedings of the 2006 EuroSys Conference, Leuven, Belgium, April 18-21, 2006, 2006

Automated Abstraction of Software.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2006

2005

Polymorphic predicate abstraction.

[BibT_eX]

[DOI]

Todd D. Millstein

ACM Trans. Program. Lang. Syst., 2005

The Verified Software Challenge: A Call for a Holistic Approach to Reliability.

[BibT_eX]

[DOI]

Proceedings of the Verified Software: Theories, 2005

Zap: Automated Theorem Proving for Software Analysis.

[BibT_eX]

[DOI]

Shuvendu K. Lahiri

Madanlal Musuvathi

Proceedings of the Logic for Programming, 2005

Static analysis tools as early indicators of pre-release defect density.

[BibT_eX]

[DOI]

Proceedings of the 27th International Conference on Software Engineering (ICSE 2005), 2005

Use of relative code churn measures to predict system defect density.

[BibT_eX]

[DOI]

Proceedings of the 27th International Conference on Software Engineering (ICSE 2005), 2005

05261 Abstracts Collection - Multi-Version Program Analysis.

[BibT_eX]

[DOI]

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

05261 Summary - Multi-Version Program Analysis.

[BibT_eX]

[DOI]

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

Abstraction for Falsification.

[BibT_eX]

[DOI]

Greta Yorsh

Proceedings of the Computer Aided Verification, 17th International Conference, 2005

2004

Righting Software.

[BibT_eX]

[DOI]

Ramanathan Venkatapathy

IEEE Softw., 2004

Automatic Creation of Environment Models via Training.

[BibT_eX]

[DOI]

Vladimir Levin

Fei Xie

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004

Refining Approximations in Software Predicate Abstraction.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004

Reasoning About Systems with Transition Fairness.

[BibT_eX]

[DOI]

Benjamin Aminof

Proceedings of the Logic for Programming, 2004

SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft.

[BibT_eX]

[DOI]

Proceedings of the Integrated Formal Methods, 4th International Conference, 2004

A Theory of Predicate-Complete Test Coverage and Generation.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Components and Objects, 2004

Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 16th International Conference, 2004

2003

Boolean and Cartesian abstraction for model checking C programs.

[BibT_eX]

[DOI]

Andreas Podelski

Int. J. Softw. Tools Technol. Transf., 2003

From symptom to cause: localizing errors in counterexample traces.

[BibT_eX]

[DOI]

Mayur Naik

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.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 2002

Relative Completeness of Abstraction Refinement for Software Model Checking.

[BibT_eX]

[DOI]

Andreas Podelski

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2002

Speeding Up Dataflow Analysis Using Flow-Insensitive Pointer Analysis.

[BibT_eX]

[DOI]

Proceedings of the Static Analysis, 9th International Symposium, 2002

The SLAM project: debugging system software via static analysis.

[BibT_eX]

[DOI]

Proceedings of the Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2002

Secrets of Software Model Checking.

[BibT_eX]

[DOI]

Proceedings of the AGP 2002: Proceedings of the Joint Conference on Declarative Programming, 2002

2001

SIGPLANet - A Modest Proposal for SIGPLAN in the 21st Century.

[BibT_eX]

[DOI]

Hans-Juergen Boehm

ACM SIGPLAN Notices, 2001

Parameterized Verification of Multithreaded Software Libraries.

[BibT_eX]

[DOI]

Sagar Chaki

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2001

Automatically Validating Temporal Safety Properties of Interfaces.

[BibT_eX]

[DOI]

Proceedings of the Model Checking Software, 2001

Bebop: a path-sensitive interprocedural dataflow engine.

[BibT_eX]

[DOI]

Proceedings of the 2001 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis For Software Tools and Engineering, 2001

The SLAM Toolkit.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 13th International Conference, 2001

2000

State Generation and Automated Class Testing.

[BibT_eX]

[DOI]

Softw. Test. Verification Reliab., 2000

Sisl: Several Interfaces, Single Logic.

[BibT_eX]

[DOI]

Lalita Jategaonkar Jagadeesan

Christopher Colby

Peter J. Danielsen

Int. J. Speech Technol., 2000

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

[BibT_eX]

[DOI]

Computer, 2000

Speech-enabled services using TelePortalTM software and VoiceXMLstar.

[BibT_eX]

[DOI]

Bell Labs Tech. J., 2000

Bebop: A Symbolic Model Checker for Boolean Programs.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 1999

Paths between Imperative and Functional Programming.

[BibT_eX]

[DOI]

ACM SIGPLAN Notices, 1999

Using Version Control Data to Evaluate the Impact of Software Tools.

[BibT_eX]

[DOI]

Proceedings of the 1999 International Conference on Software Engineering, 1999

Coping with Type Casts in C.

[BibT_eX]

[DOI]

Michael Siff

Satish Chandra

Krishna Kunchithapadam

Thomas W. Reps

Proceedings of the Software Engineering, 1999

The Concept of Dynamic Analysis.

[BibT_eX]

[DOI]

Proceedings of the Software Engineering, 1999

1998

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

[BibT_eX]

[DOI]

Yih-Farn Chen

Eleftherios Koutsofios

World Wide Web, 1998

Edge Profiling versus Path Profiling: The Showdown.

[BibT_eX]

[DOI]

Peter Mataga

Shmuel Sagiv

Proceedings of the POPL '98, 1998

On the Limit of Control Flow Analysis for Regression Test Selection.

[BibT_eX]

[DOI]

Proceedings of ACM SIGSOFT International Symposium on Software Testing and Analysis, 1998

1997

Integrated web and telephone service creation.

[BibT_eX]

[DOI]

J. Christopher Ramming

Kenneth Rehor

Curtis Tuckey

Bell Labs Tech. J., 1997

Exploiting Hardware Performance Counters with Flow and Context Sensitive Profiling.

[BibT_eX]

[DOI]

Glenn Ammons

Proceedings of the ACM SIGPLAN '97 Conference on Programming Language Design and Implementation (PLDI), 1997

Visualizing Interactions in Program Executions.

[BibT_eX]

[DOI]

Dean F. Jerding

John T. Stasko

Proceedings of the Pulling Together, 1997

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

[BibT_eX]

[DOI]

Proceedings of the Software Engineering, 1997

Experience with a Domain Specific Language for Form-based Services.

[BibT_eX]

[DOI]

Proceedings of the Conference on Domain-Specific Languages, 1997

1996

Software Visualization in the Large.

[BibT_eX]

[DOI]

Stephen G. Eick

Computer, 1996

WebGUIDE: Querying and Navigating Changes in Web Repositories.

[BibT_eX]

[DOI]

Yih-Farn Chen

Eleftherios Koutsofios

Comput. Networks, 1996

Tracking and Viewing Changes on the Web.

[BibT_eX]

Proceedings of the USENIX Annual Technical Conference, 1996

Efficient Path Profiling.

[BibT_eX]

[DOI]

Proceedings of the 29th Annual IEEE/ACM International Symposium on Microarchitecture, 1996

An Internet Difference Engine and its Applications.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Supercomputing '95, San Diego, CA, USA, December 4-8, 1995, 1995

1994

Optimally Profiling and Tracing Programs.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 1994

Efficient Counting Program Events with Support for On-Line Queries.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 1994

Rewriting Executable Files to Measure Program Behavior.

[BibT_eX]

[DOI]

Softw. Pract. Exp., 1994

Visualizing Program Slices.

[BibT_eX]

[DOI]

Stephen G. Eick

Proceedings of the Proceedings IEEE Symposium on Visual Languages, 1994

1993

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

[BibT_eX]

[DOI]

LOPLAS, 1993

Branch Prediction For Free.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGPLAN'93 Conference on Programming Language Design and Implementation (PLDI), 1993

Slicing Programs with Arbitrary Control-flow.

[BibT_eX]

[DOI]