Polynomial programs are imperative programs with real-valued variables, i.e. imperative programs in which all expressions appearing in assignments, conditions, and guards are polynomials over program variables. A template-based synthesis of polynomial programs refers to the synthesis of missing polynomial expressions of a polynomial program given the pre and post-condition of the program. The template-based synthesis problem in general can be readily reduced to solving a logical formula with a quantifier alternation. However, solving these logical formulas with quantifier alternation is not practical using modern SMT solvers as they usually time out on even the simplest templates. In this talk, we will discuss our sound and semi-complete algorithm, based on techniques from linear algebra and algebraic geometry such as Farkas’ Lemma, Handelman’s Theorem, and Positivstellensatz, that can be used to eliminate the quantifier alteration and make the problem feasible to be solved by SMT solvers.