Lifting Numerical Abstract Domains to Heap-manipulating Programs - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Pré-Publication, Document De Travail Année : 2013

Lifting Numerical Abstract Domains to Heap-manipulating Programs

Résumé

The abstract interpretation literature is rich with numerical abstract domains that allow to infer numerical properties on scalar program variables. Unfortunately, lifting this domains to heap-manipulating programs is not obvious. On the other hand, points-to analyses have been intensively studied and some scale to very large programs but without inferring any numerical properties. We propose a framework based on the theory of abstract interpretation that is able to combine existing numerical domains and points-to analyses in a modular way. Our approach allows us to prove the soundness of the combined analysis based on the soundness hypotheses of the existing analyses, and it also facilitates the modular implementation of the analysis. We have prototyped this approach using the \SOOT framework for pointer analyses and the PPL library as numerical domains. Our experiments on the DaCapo benchmark suite show that the combined analysis discovers significantly more numerical invariants than traditional numerical domains with modest time overhead.
Fichier principal
Vignette du fichier
nump_main.pdf (522.78 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-00809826 , version 1 (09-04-2013)
hal-00809826 , version 2 (20-12-2013)
hal-00809826 , version 3 (20-12-2013)

Identifiants

  • HAL Id : hal-00809826 , version 1

Citer

Zhoulai Fu, Thomas Jensen, David Pichardie. Lifting Numerical Abstract Domains to Heap-manipulating Programs. 2013. ⟨hal-00809826v1⟩

Collections

CNRS INRIA IRISA
296 Consultations
487 Téléchargements

Partager

Gmail Facebook X LinkedIn More