Skip to Main content Skip to Navigation
Conference papers

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.
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 : Thursday, September 24, 2020 - 4:36:01 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

263

Files downloads

493