Thursday, November 30, 2017 - 3:30pm to 4:30pm
Location:Traffic21 Classroom 6501 Gates Hillman Centers
Speaker:RUBEN MARTINS, Systems Scientist https://www.linkedin.com/in/ruben-martins-404aa1b0
Scaling up Component-based Program Synthesis
In recent years, there has been significant interest in component-based program synthesis, in which the goal is to automatically generate programs from a set of components that meet a high-level specification provided by the user. Automated program synthesis has proven to be useful to both end-users and programmers. For instance, program synthesis has been used to automate tedious tasks that arise in everyday life, such as string manipulations in spreadsheets or data wrangling tasks in R. Program synthesis has also been used for improving programmer productivity by automatically completing parts of a program or helping programmers use complex APIs.
In this talk, I will present techniques for scaling up component-based program synthesis to larger and more complex pieces of code. I will start by presenting a novel-type directed algorithm based on Petri-nets that can handle thousands of components. Next, I will show how we can combine type-directed search with SMT-based deduction to further prune the search space. Finally, I will talk on our ongoing work on conflict-driven synthesis that is capable of learning from past mistakes. Learning had a tremendous effect on the performance of constraint solvers and when applied to program synthesis may allows us to tackle real-world problems that are beyond the reach of current program synthesis tools.
Ruben Martins is a Systems Scientist at the Carnegie Mellon University. Prior to joining CMU, he was a postdoctoral researcher at UT Austin where he pushed the frontiers of component-based program synthesis with constraint solving. Before UT Austin, he was a postdoctoral researcher at the University of Oxford, UK where he worked on bounded model checking for software verification. He received his PhD with honors from the University of Lisbon, Portugal in 2013. His research aims to improve constraint solvers and broaden their applicability in program analysis, synthesis, and security. Dr. Martins has developed several award winning solvers and has consistently improved the state-of-the-art in MaxSAT solving. He is currently the main developer of Open-WBO: an open source MaxSAT solver that won several awards in the MaxSAT competitions.