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. The motivation is twofold. First, narrowing the space of implementations makes the synthesis problem more tractable. Second, providing a specific syntax can potentially lead to better optimizations.

### The Problem

A Syntax-Guided Synthesis problem (SyGuS, in short) is specified with respect to a background theory , such as Linear-Integer-Arithmetic (LIA), that fixes the types of variables, operations on types, and their interpretation.

To synthesize a function of a given type, the input consists of two constraints:

**(1)** a *semantic constraint* given as a formula built from
symbols in theory along with , and
**(2)** a *syntactic constraint* given as a (possibly infinite) set
of expressions from specified by a context-free grammar.

The computational problem then is to find an implementation for the function ,
*i.e.* an expression such that the formula is valid.

### The Competition

The SyGuS competition (SyGuS-Comp) will allow solvers for syntax-guided synthesis problems to compete on a large collection of benchmarks. The motivation behind the competition is to propagate and advance research and tools on the subject.

Planning for the 6^{th} SyGuS-Comp will commence around January 2019.
Feel free to reach us at sygus-organizers@seas.upenn.edu with questions and suggestions.