@techreport{TR-IC-08-31,
  number = {TR-IC-08-31},
  author = {Nadir Matringe and Arnaldo Vieira-Moura and Rachid Rebiha},
  title = {Endomorphism for Non-Trivial Semi-Algebraic Loop Invariant
Generation},
  month = {November},
  year = {2008}, 
  institution = {Institute of Computing, University of Campinas},
  note = {In English, 25 pages.
    \par\selectlanguage{english}\textbf{Abstract}
    Non-linear loop invariant generation have seen tremendous progress
    in recent years.  However, the  weakness of these approach is that
    they are limited  to linear (affine) system, and  they often relay
    on trivial polynomial invariant (null or constant).  Moreover, for
    programs  with  loops  that  describe multivariate  polynomial  or
    multivariate fractional system, no  method is known to lend itself
    to  non-trivial non-linear  invariant.  In  order to  automate the
    generation of  non-trivial multivariate polynomial  invariant, one
    needs   to  handle  initiation   and  consecution   condition  for
    non-linear   (algebraic)   loop.    We  demonstrate   a   powerful
    computational complete method that  encodes these conditions for a
    candidate  invariant  (a  multivariate polynomial  assertion  with
    indeterminate  coefficients)   into  a  set   of  multi-parametric
    constraints  such  that   all  solutions  identify  a  non-trivial
    non-linear loop  invariant. Then,  we provide a  complete decision
    procedure for  this constraint-solving  problem. For each  type of
    loop (affine, polynomial,  fractional system) we present necessary
    and  sufficient  conditions   for  the  existence  of  non-trivial
    non-linear loop invariant and  we identify a large decidable class
    together with  undecidable class. Without  computing Grobner bases
    or using quantifier elimination techniques we show that our method
    generates  stronger invariant,  hereby  circumventing difficulties
    met by recent approach.
  }
}