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_16: Although every terminating loop has a ranking function, not every loop has a ranking function of a restricted form, such as a lexicographic tuple of polynomials over program variables. We propose polyranking functions as a generalization of ranking functions for analyzing termination of loops. We dene lexicographic polyranking functions in a general context and then specialize their synthesis and application to loops with polynomial guards and assignments of polynomial expressions. Finally, we demonstrate that our prototype implementation for C source code scales to large software projects, proving termination for a high percentage of targeted loops.
Polynomial lasso programs have also received some attention regarding the analysis of their termination properties. Bradley, Manna and Sipma use finite difference arithmetic to compute lexicographic polynomial ranking functions for polynomial lasso programs @cite_16 .