I am a computer scientist at the University of California, Berkeley. My research focuses on improving software design and development through automation. I have developed a variety of automated techniques for analyzing software artifacts, including specifications, programs, tests, and memory models. I am currently working on a lightweight, extensible framework for program synthesis.
- A high-level functional language embedded in Racket. Rosette extends Racket with the ability to execute, validate, debug and complete partial programs by compiling them to constraints, which are then solved using off-the-shelf decision procedures. [ CAV'12 tutorial; BOOGIE'12 talk ]
- A language and a solver for specifying and instantiating multidimensional data models. Given a set of model constraints and a set of statistical constraints, TestBlox produces a large sample database that satisfies (a maximal subset of) the model, and that has the desired statistical properties. [FSE'12; Technical Report]
- A debugging tool that uses an angelic oracle, implemented by a symbolic execution engine, to identify likely causes of test failures. [ICSE'11]
- A SAT-based framework for checking axiomatic specifications of memory models. MemSAT is the first tool to automatically check the Java Memory Model against its published causality tests. [PLDI'10]
- An efficient constraint solver for relational logic with many applications, including design analysis, code checking, test-case generation, and declarative configuration. [PhD; FM'08; TACAS'07]
- Distinguished paper award at FSE 2012, November 11-16, 2012.
- Co-teaching a graduate course on program synthesis with Rastislav Bodik, Fall 2012.
- Invited tutorial at CAV'12 (with Rastislav Bodik), July 09, 2012.
- Invited talk at BOOGIE'12, July 08, 2012.
- Observer at the 52nd IFIP WG 2.4 meeting in Vadstena, Sweden, May 20-25, 2012.
- OOPSLA'12 Program Committee.
- Kodkod tutorial at the Dagstuhl Seminar on Software Synthesis, April 9-13, 2012.
- PLDI'12 Program Comittee.