To the best of our knowledge, existing synthesis approaches are restricted to
linear invariants, see for instance [1]}, whereas our work supports loop
synthesis from non-linear polynomial properties.
Existing approaches to SyGuS-based
synthesis [2]}
differ in the (a) logical expressiveness of input
specifications,
(b) restrictions of the solutions space of programs to be
synthesized and (c) search strategies for solutions during synthesis.
The key difference between our work and the
state-of-the-art in synthesis is three-fold: (i) we consider logical
specifications as (non-linear) polynomial invariant relations, (ii)
synthesize loops with non-linear behaviour, and (iii)
precisely characterize the set of all such loops to be synthesized. To the
best of our knowledge, existing approaches are restricted to linear
invariants, see e.g. [1]}, and no other approach can
automatically synthesize loops from
polynomial invariants.
In what
follows, we discuss approaches that are mostly related to our work.
focusing only on works handling loops and/or
recursion.
