DATA FLOW-ANALYSIS AS MODEL CHECKING

The paper develops a framework that is based on 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 implementations of DFA-algorithms from modal specifications by partially evaluating a specific model checker with respect to 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. - The framework is illustrated by means of a real life example: the problem of determining optimal computation points within flow graphs.