  We present an algorithm for synthesizing program loops satisfying a given
polynomial loop invariant. The class of loops we consider can be modeled by a
system of algebraic recurrence equations with constant coefficients. 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 program verification, as well as generating number
sequences from algebraic relations. We implemented our work in the Absynth tool
and report on our initial experiments with loop synthesis.
