Data flow analysis as model checking

Abstract

The paper develops the idea that modal logic provides an appropriate framework for the specification of data flow analysis (DFA) algorithms as soon as programs are represented as models of the logic. This can be exploited to construct a DFA-generator that generates efficient DFA-algorithms from modal specifications by partially evaluating a specific model checker wrt the specifying modal formula. Moreover, the use of a modal logic as specification language for DFA-algorithms supports the compositional development of specifications and structured proofs of properties of DFA-algorithms. These ideas are applied to the problem of determining optimal computation points within flow graphs.