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 implementations.

The commonalities of these recent works has been identified, formalized and coined as the syntax-guided synthesis problem [1, 2]. Syntax-Guided Synthesis (SyGuS) is the computational problem of finding an implementation f that meets both a semantic constraint given by a logical formula φ in a background theory T , and a syntactic constraint given by a grammar G, which specifies the allowed set of candidate implementations. Such a synthesis problem can be formally defined in SyGuS-IF [3], a language that is built on top of SMT-LIB. In order to facilitate, bring together and accelerate research and development of efficient solvers for SyGuS the Syntax-Guided Synthesis Competition (SyGuS-Comp) was initiated.

In this tutorial we will explain the problem of syntax-guided synthesis and elaborate on several distinct approaches for solving it. The tutorial will be accompanied by examples ranging from different domain areas such as bit-vector manipulations, invariant synthesis, compiler optimization and robot motion planning. The tutorial will include an hands on session in which the participants will experiment with formalizing problems in SyGuS, running them on the StarExec web-platform and examining the results from the solvers participating in this year’s competition.

[1] R. Alur, R. Bodík, E. Dallal, D. Fisman, P. Garg, G. Juniwal, H. Kress-Gazit, P. Madhusudan, M. K. Martin, M. Raghothaman, S. Saha, S. Seshia, R. Singh, A. Solar-Lezama, E. Torlak, and A. Udupa. Syntax-guided synthesis. In Dependable Software Systems Engineering, volume 40, pages 1–25. IOS Press, 2015.

[2] R. Alur, R. Bodík, G. Juniwal, M. K. Martin, M. Raghothaman, S. Seshia, R. Singh, A. Solar-Lezama, E. Torlak, and A. Udupa. Syntax-guided synthesis. In Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013, pages 1–8, 2013.

[3] M. Raghothaman and A. Udupa. Language to specify syntax-guided synthesis problems. CoRR, abs/1405.5590, 2014.