I am a research software engineer on the PROSE Team at Microsoft, where we build program synthesizers that help users create programs without writing code: users give examples of the computation, and our synthesizers search for programs consistent with those examples.
I earned my PhD in Computer Science from the University of California, San Diego, where I was a member of the Programming Systems Group advised by Sorin Lerner. My graduate work focused on programming language techniques to help developers build complex software with fewer mistakes, drawing from the areas of program synthesis, analysis, and verification.
Prior to graduate school, I was a circuit design engineer at Intel, where I worked on L3 caches for two different Itanium microprocessors. My bachelor's degree is in Electrical and Computer Engineering from Cornell University.
Synthesizing Edit Suggestions
We present Blue-Pencil, a modeless system that observes users as they edit documents, silently identifies repetitive changes, and automatically suggests similar transformations that could apply at other locations. This technology has been released in Visual Studio 2019 for C# as IntelliCode Refactorings.
Synthesizing Parsers by Example
We implement a graphical development environment for synthesizing parsers by example. The user presents examples simply by selecting and labeling sample text in a graphical text editor. An underlying synthesis engine then constructs or refines lexer rules and grammar productions based on the supplied examples, all without requiring the user to write code.
C-to-Verilog Equivalence Checking
High-Level Synthesis (HLS) tools translate specifications in high-level languages like C/C++ down to hardware description languages such as Verilog. We implement an equivalence checker called VTV that verifies the correctness of the HLS translation process, then use it to validate a body of programs compiled by the Xilinx Vivado HLS compiler.
GPU Kernel Test Amplification
We implement a novel analysis for verifying properties of data parallel GPU programs. The key concept behind our work is test amplification: we can use static information flow to amplify the result of a single test execution over the set of all inputs and interleavings that affect the property being verified. Using our analysis, we verify race-freedom and determinism over a large number of standard GPU kernels written in CUDA.
I was a teaching assistant for the following courses.