Widening with Thresholds for Programs with Complex Control Graphs

Abstract : The precision of an analysis based on abstract interpretation does not only depend on the abstract domain, but also on the solving method. The traditional solution is to solve iteratively abstract fixpoint equations, using extrapolation with a widening operator to make the iterations converge. Unfortunately, this extrapolation often loses crucial information for the analysis goal. A classical technique for improving the precision is ''widening with thresholds'', which bounds the extrapolation. Its benefit strongly depends on the choice of relevant thresholds. In this paper we propose a semantic-based technique for automatically inferring such thresholds, which applies to any control graph, be it intraprocedural, interprocedural or concurrent, without specific assumptions on the abstract domain. Despite its technical simplicity, our technique is able to infer the relevant thresholds in many practical cases.
Type de document :
Communication dans un congrès
Automated Technology for Verification and Analysis, ATVA'11, Oct 2011, Taipei, Taiwan. 6996, pp.492-502, 2011, LNCS. 〈10.1007/978-3-642-24372-1_38〉
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00635243
Contributeur : Bertrand Jeannet <>
Soumis le : lundi 24 octobre 2011 - 18:33:01
Dernière modification le : jeudi 11 janvier 2018 - 06:22:03
Document(s) archivé(s) le : dimanche 4 décembre 2016 - 09:49:11

Fichier

fulltext_39_.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

Collections

Citation

Lies Lakhdar-Chaouch, Bertrand Jeannet, Alain Girault. Widening with Thresholds for Programs with Complex Control Graphs. Automated Technology for Verification and Analysis, ATVA'11, Oct 2011, Taipei, Taiwan. 6996, pp.492-502, 2011, LNCS. 〈10.1007/978-3-642-24372-1_38〉. 〈inria-00635243〉

Partager

Métriques

Consultations de la notice

292

Téléchargements de fichiers

409