@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.
}
}