

Generating number sequences. Our approach provides a partial solution to
an open mathematical problem: given a polynomial relation among number
sequences, e.g.
\(f(n)^4 + 2f(n)^3f(n+1) - f(n)^2f(n+1)^2 - 2f(n)f(n+1)^3 + f(n+1)^4 = 1,\) 
synthesize algebraic recurrences defining these sequences. There exists no
complete method for solving this challenge, but we give a complete approach in
the C-finite setting parameterized by an a priori bound \(s\)  on the order of the
recurrences. For the given relation (REF ) among \(f(n)\)  and \(f(n+1)\) , our
work generates the C-finite recurrence equation \(f(n+2)=f(n+1)+f(n)\)  which
induces the Fibonacci sequence.


Program optimizations. Given a polynomial invariant, our approach
generates a PCP such that any solution to this PCP yields a loop
satisfying the given invariant.
By using additional constraints
encoding a cost function on the loops to be synthesized, our method can be
extended to synthesize loops that are optimal with respect to the considered
costs, for example synthesizing loops that use only addition in
variable updates. Consider for example Figures REF -REF : the loop body of Figure REF  uses only addition, whereas
Figure REF  implements also multiplications by
constants.


Compiler optimizations.
To reduce execution time spent within loops,
compiler optimization techniques, such as strength reduction,
aim at replacing expensive loop operations with semantically
equivalent but less expensive operations [1]}.
One such optimization within strength reduction replaces
“strong" loop multiplications by additions among program
variables. The burden of strength reductions comes however with
identifying inductive loop variables and invariants to
be used for loop optimization. Our loop synthesis method
therefore serves as a foundation for strength reduction
optimization, by converting polynomial (loop) expressions into
incremental affine (loop) computations.


Invariant generation and loop equivalence. Our approach may improve the state-of-the-art in polynomial
invariant generation, as follows. By considering a loop \(L\) , let \(I\)  denote the
polynomial loop invariant of \(L\)  generated by existing invariant generation
approaches,
such as [2]}, [3]}, [4]}, [5]}. By
using \(I\)  as our input, our technique synthesizes a loop \(L^{\prime }\)  that is
(relational) equivalent to \(L\)  in the sense that both \(L\)  and \(L^{\prime }\)  have the same
invariant \(I\) . We showcase such use case of our synthesis approach in Section REF . We further note, that our loop synthesis task can also be used to check
soundness/completeness of existing invariant generation techniques: apply
invariant generation approaches on \(L^{\prime }\)  with the goal of deriving the invariant \(I\) .


Teaching formal methods. Finally, our work can also be used in solving
formal verification challenges, as follows. By
considering examples that are not partially correct with respect to a given
invariant, the task is to revise these programs into correct ones. By
using the given invariants as inputs to our approach, we automatically infer partially correct
programs, thus allowing
users/teachers/practitioners of formal methods to repair
programs in a fully automated manner. This use-case of loop synthesis
has been deployed in our “Formal Methods in Computer Science” master
course at the TU Wien, in particular in generating and correcting
course assignments on deductive program verification, as discussed in Section REF .

