We present a method for the synthesis of polynomial lasso programs. These programs consist of a program stem, a set of transitions, and an exit condition, all in the form of algebraic assertions (conjunctions of polynomial equalities). Central to this approach is the discovery of non-linear (algebraic) loop invariants. We extend Sankaranarayanan, Sipma, and Manna's template-based approach and prove a completeness criterion. We perform program synthesis by generating a constraint whose solution is a synthesized program together with a loop invariant that proves the program's correctness. This constraint is non-linear and is passed to an SMT solver. Moreover, we can enforce the termination of the synthesized program with the support of test cases.
@cite_23: We present a static analysis that approximates the relational semantics of imperative programs by systems of low-degree polynomial equalities. Our method is based on Abstract Interpretation in a lattice of polynomial pseudo ideals - finite-dimensional vector spaces of degree-bounded polynomials that are closed under degree-bounded products. For a fixed degree bound, the sizes of bases of pseudo ideals and the lengths of chains in the lattice of pseudo ideals are bounded by polynomials in the number of program variables. Despite the approximate nature of our analysis, for several programs taken from the literature on non-linear polynomial invariant generation our method produces results that are as precise as those produced by methods based on polynomial ideals and Grobner bases.
Colón combines the two aforementioned approaches by doing the fixed point computation on ideals with linear algebra @cite_23 . He introduces the notion of pseudo-ideals to ensure termination of the fixed point computation while retaining the expressiveness of generated invariants.