The link between abstract interpretation and dataflow analysis was first exhibited by P. & R. Cousot (POPL'79) by showing that the merge over all paths and fixpoint solutions used in dataflow analysis are all abstract interpretations of (at the time finite prefix closed) sets of traces. So the equations to be solved can be derived from the program semantics (the considered example was that of available expressions).

In another direction, Bernhard Steffen established a link between data-flow analysis as model-checking (TACS'91, LNCS 536) and studied the generation of data-flow analysis algorithms from model specifications (SCP 21:115-139, 1993): the program is abstracted into a model which is checked with a modal µ-calculus formula. Abstract interpretation is used only at the flowchart node level to specify the correctness of the dataflow transfer functions.

Dave Schmidt builds upon these previous works by introducing the point of view that “an iterative data-flow analysis is a model-check of a modal logic formula on a program's abstract interpretation” (POPL'98). The idea is that the model used by Bernhard Steffen can be obtained by an abstract interpretation of a trace-based operational semantics and that the model check of the modal logic formula on this model “yield the same information as” the solution to the data-flow equations. We are not fully satisfied by this point of view because it gives the impression to have two different ways (model checking and dataflow analysis) to do the same think. In particular the presence of a bug in live variables analysis shows that the methodology does not guarantee soundness. This is because the dataflow equations are not derived by abstraction of their specification. This is a general problem with model-checking where the abstraction process is (in general) not (fully) taken into account.

We show that model-checking is an abstract interpretation and then instantiate to the modal logic formula specifying the data-flow property. Hence the data-flow equations are derived by calculus by abstraction of their specification, a point which is left informal in the previous works and will broaden our POPL'79 point of view (where the abstraction was specific to each considered example).

We first introduce a new temporal logic RTL, with a reversal operator making past and future completely symmetric. The semantics of temporal formulae is given in compositional fixpoint form. The semantics of programs is a trace-based operational semantics generated by a total transition system. We next introduce universal and existential (may be state and location partitioned) abstractions, their duals and reversals, checking a temporal formula for an operational semantics. We show how to derive the boolean model-checking equations by fixpoint abstraction (for short only the existential abstraction of forward state properties is considered).

This is finally applied to live-variables. Liveness is specified along one path. The existential abstraction classical is used to merge over some path. The classical dataflow equations are derived for this existential abstraction. Hence dead variables are correct for the universal abstraction as observed by D. Schmidt. Thus, abstract interpretation provides an unambiguous understanding of the abstraction process and the dataflow equations are correct by construction.

In conclusion, we have shown that model-checking is an abstract interpretation. By making the abstraction explicit, correctness of the model-checking is by construction and mathematically well-founded. More generally, we stress that abstract interpretation is a theory of discrete approximation of semantics, not only a peculiar static program analysis method. In this talk, we have seen that it covers both model-checking and dataflow analysis.