@techreport{TR-IC-13-04,
   number = {IC-13-04},
   author = {Rachid Rebiha and Arnaldo V. Moura and Nadir Matringe},
   title  =  {Generating  Invariants  for  Non-linear  Loops by Linear
                   Algebraic Methods},
   month = {February},
   year = {2013},
   institution = {Institute of Computing, University of Campinas},
   note = {In English, 37 pages.
    \par\selectlanguage{english}\textbf{Abstract}
       We  present  new  computational  methods  that can automate the
       discovery     and     the     strengthening    of    non-linear   
       interrelationships  among  the variables of programs containing
       non-linear  loops,  that  is,  that  give  rise to multivariate
       polynomial  and  fractional  relationships.  Our  methods  have 
       complexities  lower  than  the  mathematical foundations of the
       previous  approaches,  which  used  Grobner  basis computation,
       quantifier  elimination or cylindrical algebraic decomposition.
       We  show that the preconditions for discrete transitions can be
       viewed  as  morphisms  over a vector space of degree bounded by
       polynomials. These morphisms can, thus, be suitably represented
       by  matrices.  We  also  introduce  fractional  and  polynomial 
       consecution,   as   more   general   forms   for  approximating 
       consecution.  The  new  relaxed consecution conditions are also
       encoded  as  morphisms represented by matrices. By so doing, we
       reduce  the non-linear loop invariant generation problem to the
       computation  of eigenspaces of specific morphisms. Moreover, as
       one  of  the  main  results, we provide very general sufficient
       conditions  allowing  for the existence and computation of loop
       invariant  ideals.  As  far  as  it is our knowledge, it is the
       first  invariant  generation  methods  that handle multivariate
       fractional loops. Our algorithm also incorporates a strategy to
       guess  the  degree  bounds  which  allow  for the generation of
       ideals of non-trivial invariants.
  }
}