caa a22 4500 605516278 CHVBK 20210128100713.0 cr unu---uuuuu 210128e20151101xx s 000 0 eng 10.1007/s00165-015-0333-3 doi (NATIONALLICENCE)springer-10.1007/s00165-015-0333-3 Generating invariants for non-linear loops by linear algebraic methods [Elektronische Daten] [Rachid Rebiha, Arnaldo Moura, Nadir Matringe] 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 Gröbner basis computations, quantifier eliminations or cylindrical algebraic decompositions. 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 can 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 whole loop invariant ideals. As far as it is our knowledge, it is the first invariant generation methods that can handle multivariate fractional loops. British Computer Society, 2015 Formal methods nationallicence Invariant generation nationallicence Linear algebra nationallicence Rebiha Rachid Institute of Computing, University of Campinas, Campinas, Brazil aut Moura Arnaldo Institute of Computing, University of Campinas, Campinas, Brazil aut Matringe Nadir LMA, University of Poitiers, Poitiers, France aut Formal Aspects of Computing Springer London 27/5-6(2015-11-01), 805-829 0934-5043 27:5-6<805 2015 27 165 https://doi.org/10.1007/s00165-015-0333-3 text/html Onlinezugriff via DOI BK010053 XK010053 XK010000 Metadata rights reserved Springer special CC-BY-NC licence nationallicence 1 research-article jats NATIONALLICENCE NATIONALLICENCE NL-springer NATIONALLICENCE 856 40 https://doi.org/10.1007/s00165-015-0333-3 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Rebiha Rachid Institute of Computing, University of Campinas, Campinas, Brazil aut NATIONALLICENCE 700 1- Moura Arnaldo Institute of Computing, University of Campinas, Campinas, Brazil aut NATIONALLICENCE 700 1- Matringe Nadir LMA, University of Poitiers, Poitiers, France aut NATIONALLICENCE 773 0- Formal Aspects of Computing Springer London 27/5-6(2015-11-01), 805-829 0934-5043 27:5-6<805 2015 27 165