research group| publications| bio| cv
professional activities | twitter

I will be working for UT Austin's Department of Computer Science starting January 2020. I have a number of openings for Ph.D. students and postdocs in my new lab. If you'd like to work with me, please apply to UTCS and name me as a prospective advisor.

I gave a keynote talk on "Machine Learning as Program Synthesis" at CAV 2019. Here are the slides.


My research lies in the intersection of Formal Methods and Artificial Intelligence. Much of my recent work is on program synthesis, the problem of automatically discovering high-level programs that fit a dataset of example behaviors and also satisfy a set of logical correctness criteria. This problem can be seen as a form of machine learning in which the learned function is represented programmatically and comes with certain formal guarantees. In my view, progress on this problem can bring us closer to the goal of robust and trustworthy artificial intelligence, and has radical implications for how we think about software.

A general solution to program synthesis will imply Artificial General Intelligence, which is another way of saying that such a solution is unlikely any time soon. However, there has been a lot of recent progress on smaller-scale versions of the problem. Here are some instantiations of the problem that my collaborators and I have recently studied:

  • Synthesizing snippets of API-usage-heavy Java code given a small number of tokens that appear in the code [ICLR18]. Our solution to this problem is implemented in the Bayou system.
  • Learning functions, written in a high-level, human-interpretable, analyzable, modular programming language, that perform the sort of classification, regression or control tasks for which neural nets are typically used [NeurIPS18, ICML18].
  • Synthesizing symbolically represented policies for small control programs that can guarantee the satisfaction of a set of temporal logic requirements [POPL14-a].
  • Learning controller parameters that lead to optimal behavior and provable satisfaction of a safety property [POPL14-b].
  • Generating scripts, written in a typed functional language, for accomplishing various end-user tasks, given a small number of input-output examples [PLDI15, PLDI16, PLDI17].
  • Generating a controller for a robot, given a set of constraints that the robot must satisfy and a logical model of the robot's environment [ICRA14, RSS16, ICAPS16, AAMAS18, WAFR18].

My work approaches program synthesis using a broad range of tools, ranging from automated deduction [POPL14-a] to functional programming language abstractions [PLDI15] to deep learning [ICLR18, NeurIPS18, ICML18] to symbolic optimization [POPL14-b] to heuristic search.

Before I began working on program synthesis, I worked for many years on the related problem of program verification. My Ph.D. work was on the logical and automata-theoretic foundations of software model checking [TOPLAS11], and I spent a number of subsequent years working on analysis of quantitative program properties such as robustness [POPL10, CACM12]. I remain interested in program verification and analysis — for example, two of our recent efforts study analysis of robustness of neural networks [S&P18] and neural methods for program debugging [FSE17].

Chris Jermaine and I co-direct the Intelligent Software Systems Laboratory (ISSYL) at Rice. The mission of our lab is to bring together symbolic and statistical methods to solve a range of problems in programming systems, data management and analytics systems, and cyber-physical systems, including but not limited to program synthesis. I am a member of the Programming Languages and Software Engineering group at Rice CS, as well as Rice's cross-disciplinary Machine Learning group.


(Spring 2018) COMP 403/503: Reasoning about software

(Fall 2016, Fall 2015, Fall 2014, Spring 2014) COMP 382: Reasoning about algorithms

(Spring 2015, Fall 2013, Fall 2012) COMP 507: Computer-Aided Program Design

(Spring 2015) COMP 607: Seminar on Program Synthesis