Welcome to my web site! I am an Associate Professor of Computer Science and Engineering at UC Santa Cruz.
I'm interested in applications of logic in computer science, particularly using automated reasoning to improve the reliability of software, hardware, and cyber-physical systems (e.g. autonomous vehicles). I work in the area of formal methods, mathematical techniques for design tasks including:
- precisely specifying systems, their environments, and their requirements;
- verifying (i.e. mathematically proving) that a system satisfies its specification;
- automatically synthesizing correct implementations for systems from high-level specifications;
- testing systems in a principled way when full verification is intractable.
My research group mainly works on formal methods techniques to design and analyze autonomous systems, especially those which use machine learning to deal with the complexities of the real world. For example, we have used our Scenic probabilistic programming language to find and fix bugs in ML-based perception systems for self-driving cars; we've also explored applications of Scenic to aircraft, robots, and other kinds of systems. Another major topic of my research is algorithmic improvisation, a new approach to synthesizing systems which use randomness to enhance robustness, variety, or unpredictability while still providing formal correctness guarantees. My group works in a variety of other areas in formal methods as well, including automated theorem proving; take a look at my research page for details.