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

The Bayou project is in the news (1, 2, 3) ! We have an opening for a postdoctoral researcher in this project. If interested, send me email!


I am a formal methods (FM) researcher with a particular interest in the intersection of FM and artificial intelligence. Much of my recent work is on program synthesis, the problem of automatically discovering high-level programs that optimally fit a dataset and also guarantee a set of logical correctness criteria. In my view, progress on program synthesis is key to realizing the dream of robust and interpretable artificial intelligence, and success here can have ramifications for all of science and engineering.

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 the problem in specific domains. Here are some instantiations of the problem that my collaborators and I have recently studied:

  • Synthesizing example programs that show a developer how to use a set of APIs, given a small amount of ambiguous information about what the developer has in mind. [ICLR18]. Our solution to this problem is implemented in the Bayou system. Here's an online demo.
  • Generating scripts that accomplish various end-user tasks, from a small number of examples of what these scripts should do. [PLDI15, PLDI16, PLDI17]
  • Generating a program that controls 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]
  • 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. [Arxiv18-a, ICML18]

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, Arxiv18-a, 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