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. Most recently, I’ve been working on physical computing and CS education.  See my papers for more details.

Recent News

Recent Writing


Microsoft MakeCode

Established: September 1, 2016

Microsoft MakeCode is a joint project between Microsoft Research and Developer Division to make it simple to program microcontroller-based devices using a modern web app.  In addition to standing up programming environments for our hardware partners, we work closely with academia on a number of projects:

The BBC micro:bit and Microsoft

Established: May 28, 2015

Try our Block/JavaScript editor! The BBC and partners, including Microsoft, announce the BBC micro:bit – a pocket-sized, codeable computer that allows children to get creative with technology. Up to 1 million micro:bits will be given to every 11 or 12 year old child in Year 7 or equivalent across the UK, for free. “The simple truth is, being a maker matters. Real computing, doing not just consuming, will drive a creative revolution in this country.…

Concurrent Revisions

Established: September 15, 2010

The Revisions project introduces a novel programming model for concurrent, parallel, and distributed applications. It provides programmers with a simple, yet powerful and efficient mechanism (based on mutable snapshots and deterministic conflict resolution) to execute various application tasks in parallel even if those tasks access the same data and may exhibit read-write or write-write conflicts. To find out more about the basic idea and how it works: Read our OOPSLA 2010 paper (links for all publications…


Established: November 25, 2008

HAVOC is a tool for specifying and checking properties of systems software written in C, in the presence of pointer manipulations, unsafe casts and dynamic memory allocation. The assertion logic of HAVOC allows the expression of properties of linked lists and arrays. The main challenge addressed by the tool are (1) tradeoff between expressiveness of the assertion logic and its computational efficiency, (2) generic inference techniques to relieve users of annotation burden for large modules.

CHESS: Find and Reproduce Heisenbugs in Concurrent Programs

Established: October 1, 2008

CHESS is a tool for finding and reproducing Heisenbugs in concurrent programs. CHESS repeatedly runs a concurrent test ensuring that every run takes a different interleaving. If an interleaving results in an error, CHESS can reproduce the interleaving for improved debugging. CHESS is available for both managed and native programs.


Established: November 5, 2001

SLAM is a project for checking that software satisfies critical behavioral properties of the interfaces it uses and to aid software engineers in designing interfaces and software that ensure reliable and correct functioning. Static Driver Verifier is a tool in the Windows Driver Development Kit that uses the SLAM verification engine. "Things like even software verification, this has been the Holy Grail of computer science for many decades but now in some very key areas,…
























Static Driver Verifier Research Platform

July 2010

    Click the icon to access this download

  • Website



Recent Talks


Recent Service


I grew up in Summit, NJ, where my claim to fame was writing a game for the Apple ][ 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“.