Rice University logo
 
Top blue bar image
Post-Doctoral Researcher
 

Projects

The ultimate goal of my research is to aid the software developer by automating several programming tasks involved in development. To this end, I have worked for several years on automated program synthesis (i.e., programs that can write themselves), verification, testing and debugging.

Bayou

Bayou is a tool for automatic program synthesis and debuggin from uncertain specifications. Uncertainty arises when the programmer is not sure of the exact intended behavior of the program, but instead only provides some evidence as to the intended behavior. The evidence may be in the form of natural language (“connect to a bluetooth socket and get its input stream”), API methods that the programmer believes should be used in the code (“android.bluetooth.BluetoothSocket.connect()”), types of variables that the code should use (“java.io.InputStream”) and so on. Given these evidences, Bayou can synthesize working code that aims to satisfy the user’s intended specification. This is achieved by statistically learning specifications of code a priori from large software corpora, such as Github, and applying Bayesian theory on the learned specifications to predict the most likely specification that the programmer has in mind given the evidences. This radical new approach to program synthesis brings together traditional formal methods and machine learning techniques.

The specifications that are learned by Bayou can also be applied towards automated debugging. In this scenario the programmer already has a complete program in hand, from which we can extract various types of evidences. Using a similar Bayesian process as before, we can compute a distance measure for the program from the learned specifications given the evidences. From the hypothesis that bugs are often deviant behaviors, this measure gives us a quantitative measure of the “bugginess” of the program.

TRACER

TRACER is a general-purpose program analysis framework for precise logical reasoning. It uses the technique of symbolic execution to exhaustively search the entire execution space of a given program. Although this search space is exponential in general, and nothing can be done about it in theory, TRACER uses techniques such as interpolation to prune significant parts of the space which results in a practically feasible convergence time. For verification, it applies overapproximations (abstractions) to ensure that a “no-bug” result is always correct, and for testing it applies underapproximations (concretization) to ensure that a reported “bug” is indeed one. If the programmer is interested in a quantitative cost measure (such as execution time), TRACER uses branch-and-bound techniques to converge quickly to the solution, and if not provide precise lower and upper bounds. TRACER can also be used for optimizing a program for particular target (output) variables, using the technique of slicing.