The Fixpoint-Analysis Machine

. We present a fixpoint-analysis machine, for the efficient computation of homogeneous, hierarchical, and alternating fixpoints over regular, context-free/push-down and macro models. Applications of such fixpoint computations include intra- and interprocedural data flow analysis, model checking for various temporal logics, and the verification of behavioural relations between distributed systems. The fixpoint-analysis machine identifies an adequate (parameterized) level for a uniform treatment of all those problems, which, despite its uniformity, outperforms the `standard iteration based' special purpose tools usually by factors around 10, even if the additional compilation time is taken into account. 1 Introduction and Motivation A great number of analysis and verification problems such as abstract interpretation, data flow analysis, model checking, determination of behavioural relations between distributed systems, hardware verification and synthesis, etc., boil down to the computa..