Efficiently intertwining widening and narrowing

• A warrowing operator is constructed which combines widening and narrowing.
• Variations of standard fixpoint algorithms are equipped with the new operator.
• For the resulting solvers, termination is proven under liberal assumptions.
• Experiments indicate that precision may be increased significantly at a decent cost.

Accelerated fixpoint iteration by means of widening and narrowing is the method of choice for solving systems of equations over domains with infinite ascending chains. The strict separation into an ascending widening and a descending narrowing phase, however, may unnecessarily give up precision that cannot be recovered later. It is also unsuitable for equation systems with infinitely many unknowns — where local solving must be used.As a remedy, we present a novel operator ⍁ that combines a given widening operator ∇ with a given narrowing operator Δ. We present adapted versions of round-robin and worklist iteration as well as local and side-effecting solving algorithms for the combined operator ⍁. We prove that the resulting solvers always return sound results and are guaranteed to terminate for monotonic systems whenever only finitely many unknowns are encountered.