Bounded Fixed-Point Iteration

In the context of abstract interpretation the authors study the number of times a functional needs to be unfolded in order to give the least fixed point. For the cases of total or monotone functions they obtain an exponential bound and in the case of strict and additive (or distributive) functions they obtain a quadratic bound. These bounds are shown to be tight. Specializing the case of strict and additive functions to functionals of a form that would correspond to iterative programs they show that a linear bound is tight. This is related to several analyses studied in the literature (including strictness analysis)