The classical formulation of the program-synthesis problem is to find a program that meets a correctness specification given as a logical formula. Recent work on program synthesis and program optimization illustrates many potential benefits of allowing the user to supplement the logical specification with a syntactic template that constrains the space of allowed implementation.
In this collaborative effort we have defined a logic-based core computational problem so that different algorithmic strategies can be compared in an experimentally rigorous manner and computational advances can be easily shared across tools (such as Sketch and Transit). Based on this definition, we have organized a solvers competition SyGuS-COMP held at FLoC 2014.
- R. Alur, R. Bodik, G. Juniwal, M.M.K. Martin, M. Raghothaman, S.A. Seshia, R. Singh, A. Solar-Lezama, E. Torlak, and A. Udupa. Syntax-guided Synthesis, FMCAD 2013
- M. Raghothaman, A. Udupa. Language to Specify Syntax-Guided Synthesis Problems. CoRR abs/1405.5590 (2014)
- A. Udupa, A. Raghavan, J. Deshmukh, S. Mador-Haim, M. Martin, R. Alur: TRANSIT: Specifying Protocols with Concolic Snippets. PLDI 2013: 287-296