Data Flow Analysis
Verifying the type safety of weakly typed languages requires data-flow analysis.
Data-flow analysis is used to establish that a property is invariant at a program point wrt every possible execution trace that reaches that point.
- Constant propagation: what variables are holding constants?
- Strictness analysis: what variables are undefined at that node?
- Type analysis: verify, for all execution sequences that reach an iadd instruction, that there are two integer values on the top of stack.