Counterexample-guided
synthesis (CEGIS) [1]}, [2]}, [3]}, [4]}
refines
the
deductive synthesis approach of [5]} and restricts the search space of
programs by using templates and/or sketches [2]}. CEGIS provides an automated
approach for synthesizing programs \(P\)  from a given specification
\(S\)  [1]}, [2]}, [4]}. For doing so, CEGIS uses
input-output examples satisfying a specification \(S\)  to synthesize a candidate program \(P\) 
that is consistent with the given inputs. Correctness
of the candidate program \(P\)  with respect to \(S\)  is then checked using
verification approaches, in particular using SMT-based reasoning. If
verification fails, a counterexample is generated as an input to \(P\)  that
violates \(S\) . This counterexample is then used in conjunction with the previous
set of input-outputs to revise synthesis and generate a new candidate program
\(P\) .
CEGIS-based approaches have been extended with machine/active
learning to control the selection of (counter-) examples satisfying \(S\)  and guide
the synthesis of \(P\)  [3]}.
Unlike these methods, input
specifications to our approach are relational (invariant) properties describing
all, potentially infinite input-output examples of interest. Hence, we do not
rely on interactive refinement of our input but work with a precise
characterization of the set of input-output values of the program to be
synthesized. Similarly to sketches [2]}, [4]}, we consider loop templates restricting the
search for solutions to synthesis. Yet, our templates support non-linear
arithmetic (and hence multiplication), which is not yet the case
in [4]}, [3]}. We rely on fixed point reasoning and
properties of algebraic recurrences to encode the synthesis problem as a
constraint solving task in the theory of non-linear real arithmetic.
We precisely characterize the set of all programs
satisfying our input specification, and as such, our approach does not exploit
learning to refine program candidates. On the other hand, our programming model
is more restricted than [4]}, [3]} in various aspects:
we only handle simple loops and only consider numeric data types and operations.
