third and fourth competitions consisted, in addition to these three tracks, the PBE track for programming by examples. The PBE track restricts semantic constraints to be based upon only input–output examples. This track is divided into two: benchmarks using the BV logic, and benchmarks manipulating strings expressed in the SLIA logic.

The ESolver based on the enumerative search strategy described previously won the first competition. Since then a number of researchers have proposed new solution strategies. For instance, the ICE-DT solver is specialized to learning invariants based on a novel idea of generalizing from implication counterexamples (as opposed just positive and negative examples common in classical learning), and won the INV track in recent competitions, 8 and the strategy to solve alternation of quantifiers within the SMT solver CVC4 was modified to produce witness functions that match the syntactic template leading to a SyGuS solver that is the most effective current solver for the CLIA and PBE-String tracks. 25 The winner of the general track in the 2017 competition is EUSolver, which we will explore.

State of the Art

The formalization of the SyGuS problem and organization of the annual competition of solvers has been a catalyst for research in search-based program synthesis. We first give an overview of the progress in solver technology, then describe the solution strategy employed by the current winner, and explain a novel application of SyGuS to synthesis of cryptographic circuits resistant to timing attacks.

Evolution of SyGuS solvers. The capabilities of SyGuS solvers are improving from competition to competition. For instance, all instances of the ICFP benchmarks were solved in 2017 competition, most in less than 10 seconds. In contrast, none of these were solved in the first competition, and in the original ICFP competition, some of these benchmarks were solved by the participants using enormously large compute clusters.

As another example, recall the
example given earlier of synthesizing
the maximum of two numbers using
the grammar Exp3. For any number n,
we can similarly write a specification
for computing the maximum of n
input arguments. In the first competi-
tion all solvers were able to solve for n
= 2, only one solver was able to solve
for n = 3 and none could solve for n = 4.
The 2017 solvers are capable of solv-
ing for n ≤ 21. Note that the size of the
minimal expression grows quadrati-
cally with n. The size of the expression
generated for n = 21 is 1621. With
regard to the time to solve these
benchmarks, instances with n ≤ 10
are solved within 5s, whereas the solu-
tion for n = 21 required 2100 s.
Trying to understand which SyGuS
instances are easily solved by current
SyGuS solvers, we recall different
aspects of a SyGuS instance: (i) The
grammar can be very general or very
restrictive, depending on the size of
the set of syntactically allowed expres-
sions. (ii) The specification can
require a single or multiple functions
to be simultaneously synthesized. (iii)
The specification can be complete or
partial depending on whether the set
of semantic solutions is a singleton or
not. (iv) The grammar may or may not
allow the use of let for specifying
auxiliary variables. (v) When the spec-
ification has several invocations of
the function to be synthesized, all
invocations may be exactly the same
(in the sense that the sequence of
parameters is the same in all) or there
may be different ways in which the
function is invoked. We refer to the
former as single invocation and to the
latter as multiple invocation. 25 The cat-
egories of benchmarks in which state-
of-the-art solvers excel are those with
a single function invocation, a single
function to synthesize, a complete
specification, no use of let, and a
restricted grammar. Benchmarks of
the CLIA and invariant generation
tracks are also easily handled by cur-
rent solvers, in spite of their grammar
being general.
Enumerative search with decision
trees. When the grammar specifying
the set of allowed expressions
includes conditionals, the desired
solution is typically a tree whose inter-
nal nodes are labeled with tests used
in conditionals and leaves are labeled
with test-free expressions. The key
The formalization of
the SyGuS problem
and organization
of the annual
competition of
solvers has been
a catalyst for
research in search-
based program
synthesis.