Skip to Main content Skip to Navigation
Conference papers

Convex invariant refinement by control node splitting: a heuristic approach

Vivien Maisonneuve 1, * 
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [27 references]  Display  Hide  Download

https://hal-mines-paristech.archives-ouvertes.fr/hal-00833344
Contributor : Bibliothèque MINES ParisTech Connect in order to contact the contributor
Submitted on : Wednesday, June 12, 2013 - 3:28:51 PM
Last modification on : Wednesday, November 17, 2021 - 12:31:43 PM
Long-term archiving on: : Tuesday, April 4, 2017 - 8:26:55 PM

File

nodesplit.pdf
Files produced by the author(s)

Identifiers

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⟩

Share

Metrics

Record views

74

Files downloads

246