Generating Data Flow Analysis Algorithms from Modal Specifications
B. Steffen
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.