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

David Cachera 1 Thomas Jensen 1 Arnaud Jobin 1 Florent Kirchner 2
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
2 LIST - Laboratoire d'Intégration des Systèmes et des Technologies
Abstract : We propose 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 like 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 all loop invariants reported previously in the literature, and executes significantly faster than implementations using Gröbner bases.
Type de document :
Communication dans un congrès
SAS - 19th International Static Analysis Symposium - 2012, Sep 2012, Deauville, France. 2012
Liste complète des métadonnées
https://hal.inria.fr/hal-00758890
Contributeur : David Cachera <>
Soumis le : jeudi 29 novembre 2012 - 15:11:51
Dernière modification le : mercredi 11 avril 2018 - 01:51:19

Identifiants

  • HAL Id : hal-00758890, version 1

Collections

INRIA | IRISA | IRISA-D4 | CEA | DRT | UR1-UFR-ISTIC | LIST | UNIV-RENNES | INRIA-RENGRE

Citation

David Cachera, Thomas Jensen, Arnaud Jobin, Florent Kirchner. Inference of polynomial invariants for imperative programs: a farewell to Gröbner bases. SAS - 19th International Static Analysis Symposium - 2012, Sep 2012, Deauville, France. 2012. 〈hal-00758890〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

1099

Contact


archive-ouverte@inria.fr