LARA

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

ConcreteAnalysis.scala

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