Abstract
Program synthesizers are effective in practice but often brittle: when a synthesis problem admits multiple solutions, synthesizers provide little guarantees on which solution they will output, and when a problem has no solution (i.e., the problem is unrealizable), most synthesizers do not terminate and get stuck exploring an infinite search space of programs. With the goal of achieving better guarantees in program synthesis, we have designed frameworks for specifying and solving synthesis problems with quantitative objectives. Although our work applies to general synthesis problem, in this talk we describe QSyGuS, a framework for specifying and solving syntax-guided-synthesis problems with quantitative objectives on the syntax of the synthesized program (e.g., minimizing the number of ITE-operators in the synthesized program). Our solving technique is general and can be built on top of any existing synthesizer. Finally, we show that proving optimality of a synthesized program requires one to prove unrealizability of another synthesis problem (one that specifies whether a better solution exists) and present the first techniques for proving whether a syntax-guided-synthesis problem is unrealizable.