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 6th SyGuS-Comp will commence around January 2019. Feel free to reach us at sygus-organizers@seas.upenn.edu with questions and suggestions.