Convex invariant refinement by control node splitting: a heuristic approach - Mines Paris Accéder directement au contenu
Communication Dans Un Congrès Electronic Notes in Theoretical Computer Science Année : 2012

Convex invariant refinement by control node splitting: a heuristic approach

Résumé

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.
Fichier principal
Vignette du fichier
nodesplit.pdf (485.12 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00833344 , version 1 (12-06-2013)

Identifiants

Citer

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⟩
77 Consultations
270 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More