Busca avançada
Ano de início
Entree
(Referência obtida automaticamente do Web of Science, por meio da informação sobre o financiamento pela FAPESP e o número do processo correspondente, incluída na publicação pelos autores.)

Generating invariants for non-linear loops by linear algebraic methods

Texto completo
Autor(es):
Rebiha, Rachid [1] ; Moura, Arnaldo Vieira [1] ; Matringe, Nadir [2]
Número total de Autores: 3
Afiliação do(s) autor(es):
[1] Univ Estadual Campinas, Inst Comp, Campinas, SP - Brazil
[2] Univ Poitiers, LMA, Poitiers - France
Número total de Afiliações: 2
Tipo de documento: Artigo Científico
Fonte: FORMAL ASPECTS OF COMPUTING; v. 27, n. 5-6, p. 805-829, NOV 2015.
Citações Web of Science: 1
Resumo

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 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. (AU)

Processo FAPESP: 11/08947-1 - Métodos Formais Algébricos para Gerção de Invariantes.
Beneficiário:Rachid Rebiha
Modalidade de apoio: Bolsas no Brasil - Pós-Doutorado
Processo FAPESP: 13/04734-9 - Métodos formais algébricos para verificação de programas
Beneficiário:Rachid Rebiha
Modalidade de apoio: Bolsas no Exterior - Estágio de Pesquisa - Pós-Doutorado