About Me
My research is at the intersection of programming languages, software engineering and
automated reasoning. I draw on techniques from machine learning and formal methods to solve
problems in program synthesis, verification, and static analysis. My goal is to build
theoretically well-understood, rigorously evaluated, and practically useful tools to help
programmers create better software with less effort.
Some recent projects that I am excited about:
- Semantic regular expressions. They combine the syntactic
pattern matching ability of classical regular expressions with the ability to consult
external oracles (think LLMs). Lots of questions. For e.g.: Can we efficiently test
membership (i.e., build something like grep)? How can we most frugally use the oracle? Can
we efficiently sample strings? See our recent
preprint.
- Subspecifications. Over the last fifty years, programming language
and formal methods researchers have developed a range of sophisticated verification and
synthesis algorithms. There has been much less work asking whether programmers can
understand this code. Subspecs are our attempt at answering this question. See our papers
at OOPSLA 2023,
VLHCC 2024 and
HotNets 2024, and a more recent
preprint applying the idea to sequential circuits.
- Bayesian program reasoning. Program analysis—finding bugs, localizing
faults, reasoning about code (more generally)—is a difficult job. Rice's theorem,
soundness, precision, scalability, all that. Can we build better program analyzers if we
account for uncertainty during the reasoning process? We've used the idea to account for
user feedback, to incrementally analyze changes to code, and to incorporate empirical
observations from test executions. See our papers at
PLDI 2018, PLDI 2019,
FSE 2021, and
ICSE 2022.
- Synthesizing Datalog programs. Datalog programs (sets of universally
quantified Horn clauses) are amazing: It is easy to precisely state their meaning
(in the simplest case, they're just if-then rules, repeatedly applied until fixpoint). A
lot of program reasoning processes can be described using these Horn clauses. What would
it take to automatically synthesize such rules? We've published papers on this topic at
IJCAI 2019,
POPL 2020, PLDI 2021,
and at OOPSLA 2023. One ambition is to automatically
synthesize program analyzers. See our paper at
UIST 2021. I've also contributed to a few papers on
improving the underlying Datalog solver itself:
PPDP 2021 and
PADL 2023.
I was previously affiliated with the University of Pennsylvania, where I was advised by
Rajeev Alur for my Ph.D., and was later a
postdoc working with Mayur Naik. During this
time, I developed the Bingo and Drake probabilistic static analysis frameworks, contributed
to formalizing the SyGuS synthesis framework, and
designed domain-specific languages and programming abstractions for stream processing
systems.
