Compared to works on invariant generation [1]}, [2]}, [3]}, [4]},
the only common aspect between these works and our synthesis
method is the use of linear recurrences to capture the functional
behavior of program loops. Yet, our work is conceptually different
from [1]}, [2]}, [3]}, [4]},
as
we reverse engineer invariant generation and do not rely on the ideal structure/Zariski closure of
polynomial invariants. We do not use ideal theory nor Gröbner bases
computation to generate invariants from loops; rather, we generate
loops from invariants by formulating and solving PCPs.
