Inference of polynomial invariants for imperative programs: a farewell to Gröbner bases

Abstract : The article presents a static analysis for computing polynomial invariants for imperative programs. The analysis is derived from an abstract interpretation of a backwards semantics, and computes pre-conditions for equalities of the form g = 0 to hold at the end of execution. A distinguishing feature of the technique is that it computes polynomial loop invariants without resorting to Gröbner base computations. The analysis uses remainder computations over parameterized polynomials in order to handle conditionals and loops efficiently. The algorithm can analyse and find a large majority of loop invariants reported pre- viously in the literature, and executes significantly faster than implementations using Gröbner bases.
Type de document :
Article dans une revue
Science of Computer Programming, Elsevier, 2014, 93, pp.21. 〈10.1016/j.scico.2014.02.028〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00932351
Contributeur : David Cachera <>
Soumis le : jeudi 16 janvier 2014 - 17:34:46
Dernière modification le : mardi 16 janvier 2018 - 15:54:15

Identifiants

Citation

David Cachera, Thomas Jensen, Arnaud Jobin, Florent Kirchner. Inference of polynomial invariants for imperative programs: a farewell to Gröbner bases. Science of Computer Programming, Elsevier, 2014, 93, pp.21. 〈10.1016/j.scico.2014.02.028〉. 〈hal-00932351〉

Partager

Métriques

Consultations de la notice

1017