In my research, I seek to develop ways to make programming tasks easier and programmers more productive. I’m particularly interested in the user interface of programming tools, such as visualization techniques for defect detection tools, new interaction techniques for common programming tasks such as debugging, as well as program analysis that are easy to apply and understand.

Otter is a pure, source-level symbolic executor for C that allows programmers to provide C programs with symbolic variables as input, and test the program for all possible assignments to those variables. A symbolic executor runs a program much like a standard interpreter, except at conditional branches: if the conditional expression of a branch is symbolic and may be either true or false, the symbolic executor conceptually forks and explores both branches.

[ Source repository ]

Directed symbolic execution applies symbolic execution to the find a set of inputs that will cause a program to run to a particular line of code. Otter provides several techniques for directed symbolic execution: shortest-path symbolic execution (SDSE) finds the path to the target line based on the shortest path through an interprocedural control-flow graph; call-chain-backward symbolic execution (CCBSE) iteratively executes forward symbolic execution from the function containing the target line backwards up the call chain to the start of the program, and Mix-CCBSE which interleaves CCBSE with another forward strategy.

[ SAS 2011 Paper† (Presentation) ] [ Tech Report ]

† © Springer-Verlag, 2011. This is the author’s version of the work. The original publication is available at http://www.springerlink.com/ in the Proceedings of the The 18th International Static Analysis Symposium, http://dx.doi.org/10.1007/978-3-642-23702-7_11

Mix is a novel static analysis framework that allows users to trade off efficiency for precision by applying analyses of different precision—currently, type checking and symbolic execution—to different parts of source code and combining the results. Users may place typed blocks or symbolic blocks to indicate parts of code that should be analyzed by fast, but imprecise, type checking or precise, but slow, symbolic execution respectively.

The key feature of Mix is that the constituent analyses are completely standard, off-the-shelf implementations. It is only at the block boundaries that special mix rules are used to translate information between the analyses. This modularity makes it easier for static analysis designers reason about the efficiency-precision trade-off in designing static analysis tools.

[ PLDI 2010 Paper† (Presentation) ] [ Tech Report ]

† © ACM, 2010. This is the author’s version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, http://doi.acm.org/10.1145/1806596.1806645

Path Projection combines two techniques—function call inlining and path-derived code folding—to “project” the source code onto the error path. Code relevant to a path is placed close together, and makes it possible for programmers to follow a path by reading from top-to-bottom.

[ Website ] [ PASTE 2008 Paper† (Presentation) ]
[ Tech Report ]

† © ACM, 2008. This is the author’s version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in Proceedings of the 8th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, http://doi.acm.org/10.1145/1512475.1512488

Arrowlets is a JavaScript library based on arrows that makes it easy to write event-driven programs. Using Arrowlets, asynchronous event listeners, synchronous event handlers or any standard JavaScript function can be written as modular units of code and flexibly composed in many different ways. Furthermore, Arrowlets eliminates the messiness of manual callback plumbing, making it easy for programmers to understand the control-flow of event-driven programs.

[ Website ] [ DLS 2009 Paper† (Presentation) ] [ ICFP 2008 Poster (Summary) ]
[ Tech Report ]

† © ACM, 2009. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. This is a minor revision of the work published in Proceedings of the 5th Symposium on Dynamic Languages, http://doi.acm.org/10.1145/1640134.1640143