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 fix-point 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.