I work at the intersection of software engineering, formal methods, and programming languages. My research focuses on developing tools and methodologies that help people build better software more easily. I have built automated tools for analyzing and synthesizing all kinds of software artifacts, including specifications, programs, executions, test data, and memory models. I am currently working on Rosette, a new solver-aided programming language that enables programmers to easily create their own domain-specific tools for program verification, synthesis, angelic execution, and fault localization.
Please see my homepage for more information.