Program synthesis is the concept of using machines to figure out the low level error prone details of a program using the higher level insights of the programmer. Sketch is a program synthesis tool that uses a constraint-based approach to synthesis. One problem with constraint-based synthesis is that it doesn’t scale on complex programs. A solution for this problem is to do modular synthesis by solving different functions of the program separately. This requires careful delinking of dependencies between different functions. In this project, we propose to use the concept of abstraction refinement to deduce preconditions and postconditions of functions and use them to abstract the functions. This approach will achieve efficient synthesis of complex programs without requiring extra effort from programmers.

I have worked previously with Prof. Armando Solar-Lezama to develop an eclipse plugin editor for Sketch and then to implement new features in Sketch to do efficient synthesis of programs involving Algebraic Datatypes. The later project also involved synthesis of translations on programming languages and is one example of a complex program which doesn’t scale well.