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.
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 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 6th SyGuS-Comp will commence around January 2019. Feel free to reach us at firstname.lastname@example.org with questions and suggestions.