Concrete Execution as Data-Flow Analysis
For a large class of properties, the most precise data-flow analysis is program execution itself
- an element is a set of states (not just one state)
- bottom: empty set
- top: all states
If program execution terminates, so does this analysis
For other analysis we use approximations
- independent attribute analysis - set of values for each variable tracked independently - all examples with pointwise lattice
- dependent variable analysis - capture dependencies between variables as in octagon abstract domain