Improving the static analysis of loops by dynamic partitioning techniques
- 2 March 2004
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
Many static analyses aim at assigning to each control point of a program an invariant property that characterizes any state of a trace corresponding to this point. The choice of the set of control points determines the states of an execution trace for which a common property must be found. We focus on sufficient conditions to substitute one control flow graph for another during an analysis. Next, we introduce a dynamic partitioning algorithm that improves the precision of the calculated invariants by deciding dynamically how to map the states of the traces to the control points, depending on the properties resulting from the first steps of the analysis. In particular, this algorithm enables the loops to be unfolded only if this improves the precision of the final invariants. Its correctness stems from the fact that it uses legal graph substitutions.Keywords
This publication has 12 references indexed in Scilit:
- Nonuniform Alias Analysis of Recursive Data Structures and ArraysPublished by Springer Nature ,2002
- Asserting the Precision of Floating-Point Computations: A Simple Abstract InterpreterPublished by Springer Nature ,2002
- Propagation of Roundoff Errors in Finite Precision Computations: A Semantics ApproachPublished by Springer Nature ,2002
- Static Analyses of the Precision of Floating-Point OperationsPublished by Springer Nature ,2001
- Dynamic Partitioning in Analyses of Numerical PropertiesPublished by Springer Nature ,1999
- Refining Static Analyses by Trace-Based Partitioning Using Control FlowPublished by Springer Nature ,1998
- Abstract interpretation by dynamic partitioningJournal of Functional Programming, 1992
- Abstract Interpretation FrameworksJournal of Logic and Computation, 1992
- Systematic design of program analysis frameworksPublished by Association for Computing Machinery (ACM) ,1979
- Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpointsPublished by Association for Computing Machinery (ACM) ,1977