I am an associate professor in the computer science department at UC Santa Barbara. I received my Ph.D. from UT Austin in 2018, where I was advised by Isil Dillig. My group builds automated reasoning tools at the intersection of programming languages, formal verification, and security — with recent focus on zero-knowledge proof systems and safe AI agents. Our work has been recognized with multiple Distinguished/Best Paper Awards at PLDI, CHI, and ASE, and has been supported by NSF, DARPA, Google, and the Ethereum Foundation.
My research develops principled techniques — rooted in program synthesis, type theory, and constraint solving — to automatically build, verify, and secure software systems. Current focus areas include: (1) formal methods and security for AI agents, ensuring autonomous systems behave safely and correctly through verification and runtime guarantees; (2) compilers and verifiers for zero-knowledge proof circuits, where we have built tools like Tabby and Tessel that detect vulnerabilities and optimize performance in ZK systems deployed in production; (3) smart contract and DeFi security, including attack synthesis and state-inconsistency detection; and (4) synthesis-driven tools for end-user programming, such as data visualization and code transpilation. A unifying theme is combining logical reasoning with learning to push the frontier of what automated tools can guarantee.
Teaching 04
Course materials on GitHubCompilers
Students build a complete compiler in Python for ChocoPy, a statically typed subset of Python, targeting x86-64 through LLVM. Covers lexing, parsing, type checking, runtime organization, SSA, dataflow analysis, optimization, and register allocation.
Formal Methods for Agentic Programming
Graduate seminar exploring formal verification of AI coding agents. Covers agent architectures, Hoare logic, SAT/SMT solvers, static analysis, security of agentic systems, and runtime guardrails.
Programming Languages
Undergraduate course on programming language foundations. Students build a language from scratch, covering lambda calculus, operational semantics, type checking, type inference, and polymorphism.
Blockchain Technologies and Security
Hands-on exploration of blockchain systems and DeFi. Covers Ethereum, Solidity, smart contract patterns, AMMs, lending protocols, MEV, layer-2 scaling, and security case studies.
Publications 43
2014–2027 · full list on Google Scholar-
ICSE ’27
Automated Security Analysis for Agentic Workflows
-
ICSE ’27
Interpretable Security Analysis of Agent Skills
-
NDSS ’27
Revealing Semantic Gaps in Zero-Knowledge Virtual Machines via Obligation-Targeted Semantic Fuzzing
-
CCS ’26
Thunderbolt: Fast Asynchronous Off-Chain Bitcoin Transfers
- OOPSLA ’25
- ASE ’25
-
SBC ’25
Tessel: An Optimizing Compiler for Efficient Zero-Knowledge Circuits
- CCS ’24
- CCS ’24
- ASE ’24
- S&P ’24
- USENIX ’24
- ASE ’23
- PLDI ’23
- PLDI ’23
- ASE ’22
- CCS ’22
- PLDI ’22
- ASPLOS ’22
- POPL ’22
- OOPSLA ’22
- OOPSLA ’22
- S&P ’22
- FSE ’21
- CHI ’21
- ASE ’20
- ASE ’20
- CAV ’20
- POPL ’20
- ASE ’19
- FSE ’19
- OOPSLA ’19
- VLDB ’19
- PLDI ’18
- FSE ’18
- CCS ’17
- PLDI ’17
- NDSS ’17
- POPL ’17
-
FSE ’16
Hunter: Next-Generation Code Reuse for Java
- APLAS ’15
- OOPSLA ’15
Awards & Grants
- Ethereum Academic Award2025
- Ethereum Academic Award2024
- Ethereum Academic Award2023
- ACM SIGPLAN Distinguished Paper Award, PLDI2022
- ACM SIGCHI Best Paper Award, CHI2021
- Google Faculty Research Award (Security)2021
- ACM SIGSOFT Distinguished Paper Award, ASE2020
- DARPA HARDEN2022–2025
- NSF-SaTC (core) medium2019–2022
- ACM SIGPLAN Distinguished Paper Award, PLDI2018
- UT Austin Graduate School Dissertation Fellowship2018
- ACM SIGPLAN PAC award2017