ok wait, I just found this thread and I feel like everyone is missing the forest for the trees here. The entire widening debate is moot — because you should all just be using polyhedra-based abstract domains instead of intervals in the first place. Polyhedra are strictly more expressive and they make the question of "which widening heuristic" a lot more tractable because your approximations are geometrically meaningful.

Intervals are boxes. Boxes are embarrassing. A convex polyhedron can capture any linear relationship between variables — things like x + y ≤ 10 or 2x - 3y ≥ 0. You literally cannot express those with intervals. The precision gain is enormous.

Switch to polyhedra, problem solved. 😺

Welcome to the forum, PolyhedralPaws. I remember saying something very similar in my first week here. Let me walk you through why it's not that simple, with patience and love. 🐾

Yes, convex polyhedra are more expressive than intervals. That expressivity comes at a cost. A serious one. The fundamental operations on polyhedra — join (convex hull), widening, projection — are all significantly more expensive than their interval counterparts.

The big one: checking feasibility of a system of linear constraints (which you need for essentially every abstract domain operation on polyhedra) reduces to linear programming. That's polynomial, sure, but with large constant factors in practice. And computing the convex hull of two polyhedra in H-representation (constraint form) is where things get really bad. The double-description method used for conversion between H-representation and V-representation (vertices/rays) can be exponential in the worst case.

But the part that's most relevant to this thread: polyhedra widening. The standard algorithm for it (from Halbwachs's PhD thesis) operates on the constraint representation — it keeps constraints from the first polyhedron that are still satisfied by the second. Simple enough. But ensuring termination while maintaining meaningful precision is genuinely hard, and in the worst case, the chain of widenings can be EXPTIME in the number of constraints.

Intervals are embarrassing? Perhaps. But they're also fast, and in many real-world verification tasks, they're fast enough to scale to millions of lines of code. Polyhedra analyses struggle to scale past small programs without heroic engineering efforts.

The precision/complexity tradeoff is real and it does not care about your feelings. 😿

wait, EXPTIME?? that seems like a lot. Are you sure it's not just exponential space or something?

also what even is a "constraint representation" vs a "vertex representation"?? genuinely asking, I come from a model checking background, not static analysis.

ok I was going to stay out of this but the polyhedra question is my jam. Let me do a proper breakdown of the Halbwachs standard widening vs the Bagnara et al. precise widening because this comes up every six months and nobody ever links the actual papers.

═══ BACKGROUND: What is a convex polyhedron (abstract domain sense) ═══

A convex polyhedron over variables x₁,...,xₙ is a set of points defined by a finite conjunction of linear inequalities: { (x₁,...,xₙ) | Ax ≤ b }. This is the H-representation (half-space representation). The V-representation (generator/vertex representation) describes the same polyhedron as the convex hull of a set of vertices, rays, and lines. Converting between these is the "double-description" problem, and it's the source of most of the computational pain.

═══ THE HALBWACHS STANDARD WIDENING ═══

Cousot and Halbwachs introduced the polyhedral domain and its widening operator in their landmark 1978 POPL paper on automatic discovery of linear restraints among program variables. The standard widening P ∇ Q is defined as follows: you keep exactly those constraints of P that are still satisfied by all points in Q. Constraints that Q "violates" get dropped.

This is elegant and cheap — just test each constraint of P against Q. It terminates because the set of constraints can only shrink or stabilize. But it's often wildly imprecise — it throws away any constraint that Q doesn't satisfy, even if Q only barely violates it.

═══ THE BAGNARA PRECISE WIDENING ═══

Bagnara, Hill, Ricci, and Zaffanella (SAS 2003 / Science of Computer Programming 2005) addressed this head-on. Their paper "Precise Widening Operators for Convex Polyhedra" presents a framework for defining widening operators that are never less precise than the standard Halbwachs widening. The key idea: instead of just testing the constraints of P, they use a more sophisticated procedure that considers additional candidate constraints drawn from the history of iterates.

Their framework combines multiple heuristics — including widening up to a set of "landmarks" or threshold constraints, and use of the previous iterate's constraints — to achieve strictly better precision while still guaranteeing termination.

The key improvement: the standard widening may drop a constraint c from P even if Q only barely violates it, and that constraint might be crucial for the invariant you're trying to prove. Bagnara's widening is more conservative about dropping constraints — it only drops them when it's absolutely forced to by the termination requirement.

═══ COMPLEXITY CONCERNS ═══

As LatticeTabby correctly noted, the complexity is a real concern. The standard widening is cheap (polynomial per step). Bagnara's precise widening involves more expensive constraint solving at each step. More importantly: the number of widening steps before stabilization can be exponential in the number of dimensions/constraints in the worst case. This is intrinsic to the polyhedra domain — it admits infinite ascending chains, so some widening mechanism is mandatory, but the complexity of that mechanism varies.

References:

• Cousot & Halbwachs (1978) — Automatic discovery of linear restraints, POPL
• Halbwachs PhD thesis (1979) — standard widening algorithm on constraint repr.
• Bagnara, Hill, Ricci, Zaffanella (2003/2005) — Precise Widening Operators for Convex Polyhedra, SAS/SciCP
• Bagnara, Hill, Zaffanella (2008) — The Parma Polyhedra Library (PPL implementation)

See also: wiki: polyhedra widening comparison table | PPL library thread

I was inspired by GaloisCat's breakdown so I spent the last 45 minutes trying to start encoding polyhedral abstract interpretation in Coq. I defined the abstract domain as a dependent type indexed by the dimension and the constraint matrix and then immediately got hit with universe inconsistency errors. Pasting them here so someone smarter than me can tell me what I did wrong:

I think the issue is that my AbstractDomain class lives in a universe that's too small for the Polyhedron type which itself is parameterized by nat. I tried adding Universe Polymorphism but then I got:

Anyway, the conceptual point I was trying to make is that the widening operator for polyhedra is really tricky to express in a way that's both provably terminating and captures the domain structure correctly. The Coq type-checker apparently agrees that this is hard. 🙀

Has anyone successfully formalized polyhedral abstract interpretation in Coq or Isabelle? I know there's the verified static analysis thread but I didn't see polyhedra specifically discussed there.

You haven't broken Coq. You've just discovered that formalizing abstract interpretation in a dependent type theory requires being very careful about universe levels. The AbstractDomain typeclass as written is trying to be polymorphic over all types simultaneously, which causes the universe issue.

The fix is: add Set Universe Polymorphism. before your class definition, and annotate the class with @{u} universe variables explicitly. Or — honestly — just use Prop for the lattice ordering and Set for the elements, keep them at the same level. The Verasco project (a verified C static analyzer in Coq) handles this; look at their abstract domain interfaces.

Also, convex_hull for the join is going to require axioms unless you're computing it via an algorithm you've also proven correct... which is, um, a very large rabbit hole. There's a reason the verified analysis community often works with simpler domains. 🐇

Sorry for the dumb question but I've been reading this thread since post 1 and people keep saying "convex polyhedron" — I've seen it explained vaguely a few times but can someone give me a proper ELI5? Like what makes it "convex" specifically, and what does it look like in 2D and 3D? I know what a box/interval is. How does a polyhedron generalize that?

I learn best from pictures but I know this is a text forum soooo... ASCII art maybe? 🥺

ProgrammingPawsy, great question! Never apologize for asking. Here is your ASCII art explanation. 🖼️

Step 1: An interval in 1D — just a segment. The abstract value [2, 7]:

Step 2: A box (interval product) in 2D — two independent intervals. Abstract value: x ∈ [1,5], y ∈ [2,4]:

Step 3: A convex polyhedron in 2D — intersection of half-planes. Can have any slope for its sides:

The key property: CONVEXITY. A shape is convex if for any two points P and Q inside it, the entire line segment PQ is also inside it. This rules out "dents" or holes:

Why convexity matters for static analysis: If your abstract domain is closed under intersection (which polyhedra are — intersect two convex sets, get a convex set) and under linear transformations (assignments), you get a clean algebraic structure. The join (convex hull) of two polyhedra is the smallest convex set containing both — this corresponds to merging two paths in your program CFG. Everything stays geometrically tidy.

In 3D: you get actual polyhedra — tetrahedra, cubes, octahedra, etc. but with potentially many more faces, each a linear constraint aᵢx + bᵢy + cᵢz ≤ dᵢ. In n dimensions, each face is an (n-1)-dimensional hyperplane half-space. This is why operations get expensive: you have up to exponentially many vertices even with few constraints.

Does that help? See also: Abstract Domains Primer on our wiki. 🐾

Alright, wonderful discussion everyone. Welcome PolyhedralPaws — don't be discouraged, the "just use polyhedra" phase is rite of passage here. We've all been through it. 🐾

Let me try to bring some synthesis to the thread before it spirals further. We've now covered:

✦ Original thread: is widening necessary at all? (answer: for infinite-height domains, yes, for convergence)
✦ Pages 2-3: threshold widening, delay strategies, precision vs. termination
✦ This page: polyhedra domains and their widening — more precise but much costlier

I want to introduce a concept that acts as a middle ground between "just widen aggressively" and "use polyhedra for everything" — and that's "widening up to" (also called widening with thresholds).

The idea: instead of letting the widening operator go all the way to ±∞ when a constraint becomes unstable, you supply a finite set of threshold values — candidate boundaries that you believe might appear in the fixpoint — and the widening "pauses" at these thresholds before jumping to infinity. More formally, given a set of thresholds T = {t₁, t₂, ..., tₖ}:

The thresholds for polyhedra can be the set of constants appearing in the program source — branch conditions, array bounds, literal integers. This is a static set, so termination is preserved (you can only pause at finitely many thresholds before reaching the standard widen). But precision improves dramatically for programs where the fixpoint lies at or near a known constant.

This technique is used in production analyzers — Astrée uses it, and Miné's work on threshold widening for numerical domains is a key reference. It essentially threads the needle between "too aggressive" and "polyhedra-level expensive" for many real programs.

So to answer the meta-question of this thread: widening is necessary, but how you widen is a rich design space. Polyhedra give you more precision at higher cost; interval widening with good thresholds often gets you 80% of the precision at 10% of the cost.

Relevant pages: wiki: widening with thresholds | Continue to page 5 → (where AbstractKitty returns with new data from running actual experiments)