My research applies programming language techniques to help developers build complex software with fewer mistakes. My projects draw from the areas of program synthesis, analysis, and verification.
I was the primary investigator on the following projects.
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 served as teaching assistant for the following courses.
I graduated from Cornell University in Spring 2004 with a degree in Electrical and Computer Engineering and a concentration in computer architecture.
I then spent five fantastic years at Intel, where I worked with a great group of computer engineers designing cache memory systems for several generations of Itanium microprocessors. During this time I developed a curiosity for software design, and in particular, the design of VLSI development tools. My interest in programming languages began when I saw how fundamentally the choice of language influenced the structure of these tools. That initial spark grew over time until I decided to pursue my PhD studying programming languages.