Shared flowchart

Software · L5 · Fixpoint Iteration With Widening

Sign in to clone

How Kleene iteration on a dataflow lattice proceeds, and where widening intervenes on an infinite-height domain to force termination.

by @openstemUpdated Software
Initialize every program point to bottom of latticeApply transfer functions along CFG edgesMerge facts at join points: union for may, intersect for mustAny point's value changed this iteration?Apply widening operator after bounded iterationsExtrapolate unstable bound toward top/infinityLeast fixpoint reachedOptional narrowing pass to regain precisionFinal sound over-approximation returnedYes, and lattice has finite heightYes, and lattice is infinite e.g. intervalsNo: stable

We use privacy-friendly product analytics (no session recording, PII masked) to improve OpenStem. Load analytics? Privacy Policy