Program Synthesis is about constructing or synthesizing correct, performant programs from formal specifications. It is the other side of the coin from Program Verification. Instead of verifying a program after the fact, synthesis aims to construct a program which is guaranteed to be correct with respect to the specification. The approach has been used to construct, for example, efficient scheduling algorithms, planners, reactive robot controllers, bus controllers for real-world problems. My PhD was in a specific area of program synthesis, called algorithm synthesis. Currently I am working on applying program synthesis to the problem of synthesizing programs for robot planning and control. Some interesting research topics are:

Robot Plan Synthesis

The planning problem for robotics involves both motion and task planning. Simply handing a task plan over to the motion planner does not work because of possible infeasibility of the task plan at the physical level. Extending OTS heuristic planners (such as FF) to include motion planning is also difficult because of the blow-up in the size of the input. There is also useful task ordering information that is known to the programmer which would significantly reduce the search space that cannot be easily supplied to an automated planner. In addition constraints on the solution (such as the limits on the lengths or clearances of the paths the robot takes, regions it must avoid, fuel limits, etc.) are difficult to express in standard planning domain languages such as PDDL, let alone for standard heuristic planners to solve. We have introduced a novel approach that represents the underlying motion planning space using an abstraction of manipulation graphs we call placement graphs, as well as language in which the programmer can supply a plan outline. We derive a set of constraints from the plan outline and placement graph which are solved. The solution is then used to flesh out the plan outline. Our work is described in a paper we have submitted to ICRA 2014

Reactive Systems

Classical planning has treated planning as a one-shot problem in which a planning problem definition and a goal are fed to a planner which returns a plan. Increasingly, though, planning is being applied to real-world problems in which the environment can change and goals are ongoing or maintenance goals. This is called reactivity. There is ongoing research in synthesizing controllers from temporal logic specifications which can handle such situations. However, due to the complexity of the approach (doubly exponential in the size of the specification), scalability remains a problem. Handling infinite spaces (caused by numeric constraints) is also difficult. We are looking at extending our plan outline approach to such cases.


For many problems, an optimal solution is very difficult to obtain, if not unknown, even for relatively modest sized inputs. For example the 20x20 Job-Shop Problem (schedule 20 jobs, each consisting of 20 tasks) remains unsolved, over 20 years after the 10x10 problem was solved (which itself remained unsolved for almost 30 years). For problems in which the search for an optimal solution is computationally infeasible, a better alternative might be to first quickly find an acceptable feasible solution, and then rewrite that solution into a more efficient (possibly optimal) one. The arrangement is similar to how a compiler first generates code and then applies optimizations to it. I have shown how the rewrite rules that carry out such an optimization can be automatically learned for Planning problems.