  Provably correct software is one of the key challenges of our software-driven
society. Program synthesis -- the task of constructing a program satisfying a
given specification -- is one strategy for achieving this. The result of this
task is then a program which is correct by design. As in the domain of program
verification, handling loops is one of the main ingredients to a successful
synthesis procedure.
  We present an algorithm for synthesizing loops satisfying a given polynomial
loop invariant. The class of loops we are considering can be modeled by a
system of algebraic recurrence equations with constant coefficients, encoding
thus program loops with affine operations among program variables. We turn the
task of loop synthesis into a polynomial constraint problem, by precisely
characterizing the set of all loops satisfying the given invariant. We prove
soundness of our approach, as well as its completeness with respect to an a
priori fixed upper bound on the number of program variables. Our work has
applications towards synthesizing loops satisfying a given polynomial loop
invariant, program verification, as well as generating number sequences from
algebraic relations. To understand viability of the methodology and heuristics
for synthesizing loops, we implement and evaluate the method using the Absynth
tool.
