Data flow analysis is model checking of abstract interpretations

This expository paper simplifies and clarifies Steffen's depiction of data flow analysis (d.f.a.) as model checking: By employing abstract interpretation (a.i.) to generate program traces and by utilizing Kozen's modal mu-calculus to express trace properties, we express in simplest possible terms that a d.f.a. is a model check of a program's a.i. trace. In particular, the classic flow equations for bit-vector-based d.f.a.s reformat trivially into modal mu-Calculus formulas. A surprising consequence is that two of the classical d.f.a.s are exposed as unsound; this problem is analyzed and simply repaired. In the process of making the above discoveries, we clarify the relationship between a.i. and d.f.a. in terms of the often-misunderstood notion of collecting semantics and we highlight how the research areas of flow analysis, abstract interpretation, and model checking have grown together.