Fast inference of polynomial invariants for imperative programs

David Cachera 1 Thomas Jensen 1 Arnaud Jobin 1 Florent Kirchner 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : We propose an abstract interpretation based method to compute polynomial invariants for imperative programs. Our analysis is a backward propagation approach that computes preconditions for equalities like g=0 to hold at the end of execution. It extends previous work by Müller-Olm and Seidl to a language that includes both polynomial equalities and disequalities. Properties are expressed using ideals, a structure that satisfies the descending chain condition, enabling fixpoints computations to terminate without use of a widening operator. In the general case, termination is characterized using ideal membership tests and Gröbner bases computations. In order to optimize computational complexity, we propose a specialized analysis dealing with inductive invariants which ensures fast termination of fixpoints computations. The optimized procedure has been shown by experiments to work well in practice, and to be two orders of magnitude faster than the state of the art analyzer of Carbonell and Kapur.
Type de document :
[Research Report] RR-7627, INRIA. 2011, pp.31
Liste complète des métadonnées

Littérature citée [20 références]  Voir  Masquer  Télécharger
Contributeur : David Cachera <>
Soumis le : mercredi 25 mai 2011 - 15:32:12
Dernière modification le : mercredi 16 mai 2018 - 11:23:28
Document(s) archivé(s) le : vendredi 9 novembre 2012 - 12:10:52


Fichiers produits par l'(les) auteur(s)


  • HAL Id : inria-00595783, version 1


David Cachera, Thomas Jensen, Arnaud Jobin, Florent Kirchner. Fast inference of polynomial invariants for imperative programs. [Research Report] RR-7627, INRIA. 2011, pp.31. 〈inria-00595783〉



Consultations de la notice


Téléchargements de fichiers