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

Convex invariant refinement by control node splitting: a heuristic approach

Abstract : To improve the accuracy of invariants found when analyzing a transition system, we introduce an original rewriting heuristic of control flow graphs, based on a control node splitting algorithm. The transformation preserves the program behaviors, whilst allowing a finer analysis. We have carried out experiments with PIPS, a source-to-source compiler, and Aspic, an abstract interpretation tool, using 71 test cases published by Gonnord, Gulwani, Halbwachs, Jeannet & al. The number of invariants found by these tools goes up from 28 to 69 for PIPS and from 44 to 62 for Aspic when our heuristics is used as a preprocessing step. The total execution time of PIPS is only marginally increased, going up from 76 to 103s, thus showing the practical interest of our optimization technique.
Type de document :
Communication dans un congrès
Liste complète des métadonnées

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

https://hal-mines-paristech.archives-ouvertes.fr/hal-00833344
Contributeur : Bibliothèque Mines Paristech <>
Soumis le : mercredi 12 juin 2013 - 15:28:51
Dernière modification le : jeudi 24 septembre 2020 - 16:36:01
Archivage à long terme le : : mardi 4 avril 2017 - 20:26:55

Fichier

nodesplit.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Vivien Maisonneuve. Convex invariant refinement by control node splitting: a heuristic approach. Third International Workshop on Numerical and Symbolic Abstract Domains, NSAD 2011, Sep 2011, Venise, Italy. pp.49-59, ⟨10.1016/j.entcs.2012.10.007⟩. ⟨hal-00833344⟩

Partager

Métriques

Consultations de la notice

249

Téléchargements de fichiers

451