A Kleene Algebra Framework for Data Flow Analysis

Data flow analysis is concerned with the static determination of relevant properties of the execution state of programs. Using Kleene algebra we develop a general framework for the formalization of a set of well-known data flow analysis problems. This approach permits an elegant yet rigorous treatment of the data flow problems and provides an intuitive cookbook style description of the formalization. We also prove the soundness of the approach with respect to the standard approach and illustrate the method on a concrete example.