I am a research engineer at the University of California, Berkeley. My research focuses on improving software design and development through automation. I have worked on a variety of automated techniques for analyzing software artifacts, including specifications, programs, tests, and memory models. My current projects center around program synthesis for high performance computing on very small and very large machines.

current projects

TestBlox
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.
Angelina
A debugging tool that uses an angelic oracle, implemented by a symbolic execution engine, to identify likely causes of test failures. [ICSE'11]
MemSAT
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]
Kodkod
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]

recent activities