Accéder directement au contenu Accéder directement à la navigation
Communication dans un congrès

A Modular Static Analysis Approach to Affine Loop Invariants Detection

Abstract : Modular static analyzers use procedure abstractions, a.k.a. summarizations, to ensure that their execution time increases linearly with the size of analyzed programs. A similar abstraction mechanism is also used within a procedure to perform a bottom-up analysis. For instance, a sequence of instructions is abstracted by combining the abstractions of its components, or a loop is abstracted using the abstraction of its loop body: fixed point iterations for a loop can be replaced by a direct computation of the transitive closure of the loop body abstraction. More specifically, our abstraction mechanism uses affine constraints, i.e. polyhedra, to specify pre- and post-conditions as well as state transformers. We present an algorithm to compute the transitive closure of such a state transformer, and we illustrate its performance on various examples. Our algorithm is simple, based on discrete differentiation and integration: it is very different from the usual abstract interpretation fixed point computation based on widening. Experiments are carried out using previously published examples. We obtain the same results directly, without using any heuristic.
Type de document :
Communication dans un congrès
Liste complète des métadonnées

https://hal-mines-paristech.archives-ouvertes.fr/hal-00586338
Contributeur : Claire Medrala <>
Soumis le : vendredi 15 avril 2011 - 15:35:22
Dernière modification le : mercredi 14 octobre 2020 - 03:52:20

Lien texte intégral

Identifiants

Citation

Corinne Ancourt, Fabien Coelho, François Irigoin. A Modular Static Analysis Approach to Affine Loop Invariants Detection. The Second International Workshop on Numerical and Symbolic Abstract Domains, Sep 2010, Perpignan, France. pp.3-16, ⟨10.1016/j.entcs.2010.09.002⟩. ⟨hal-00586338⟩

Partager

Métriques

Consultations de la notice

172