Okay kittens, I've been meaning to post this for a while. After spending three months running benchmarks on our little analysis workbench I finally have numbers worth sharing. The question: is the Polyhedra domain actually usable in production, or is it forever condemned to "works great on toy programs" land?

Short answer: it depends catastrophically on your variable count. Long answer: read on.

Background

We compared three domains across a suite of 20 numerical benchmark programs (mix of loop-heavy C programs, control-flow-intensive kernels, and some embedded-style code). All tests run with APRON as the backend, using PPL for polyhedra, ELINA for octagons, and custom intervals. Widening enabled on all domains, Cousot-Halbwachs standard widening for polyhedra. Machine: AMD Ryzen 9 7950X, 64GB RAM. Each test has a 4-hour timeout and 16GB memory cap.

Benchmark Suite Overview

Results — Analysis Time

Precision Comparison (false alarm rate on assert-checking task, lower = better)

The precision numbers are incredible when polyhedra actually finishes. But look at B06, B07, B09. The moment variable count exceeds ~18-20 in a relational context, we're toast. This is the fundamental problem with convex polyhedra: the double description requires managing both constraint and generator representations, and conversion between them via Chernikova's algorithm can blow up doubly-exponentially in the number of variables.

My question to the forum: is there any realistic path to making polyhedra practical for programs with 20+ relational variables, or should we accept octagons as our ceiling?

Great benchmarks PolyhedralPussycat, bookmarked immediately. But I want to push back on the framing a little before the "polyhedra bad" crowd piles in (looking at you, FixpointFeline 👀).

The "doubly exponential" story gets thrown around a lot but it's worth being precise. The Chernikova algorithm converts between the H-representation (constraints) and V-representation (generators/rays) of a polyhedron. The worst-case complexity for this conversion is indeed exponential in the number of variables, but:

  V-rep complexity: O(exp(n)) generators in worst case
  H-rep complexity: O(exp(n)) constraints in worst case
  Conversion (Chernikova): O(exp(n)) per step, O(exp(n)) steps
  Effective: doubly exponential in pathological cases

The key word is pathological. For programs with sparse variable interaction graphs — i.e., most real code — the polyhedra arising during analysis stay decomposable. The ELINA work by Singh, Püschel and Vechev (POPL 2017) showed exactly this: if you exploit variable partitioning, you can get orders of magnitude speedups because most real polyhedra factor into independent subspaces.

Your B09 (gaussian_elim_6x6, 40 vars, dense interactions) is literally the worst case for polyhedra. Of course it OOMs. A dense n×n linear system has maximally interacting variables by construction. That's a benchmark designed to fail polyhedra, not a representative real-world program.

Yes: decomposed polyhedra (block-diagonal factorization), template polyhedra (fix constraint templates a priori), or sub-polyhedra domains like Pentagons or LinearRelation. None of these are as precise as full polyhedra, but they're far more scalable and much more precise than octagons for programs with genuine multi-variable invariants.

See also: the ELINA decomposed polyhedra thread and template polyhedra.

I am right here and I have opinions, as always.

GaloisCat's "it's only pathological cases" argument is the same cope I've been hearing at every SAS conference since 2015. Let me be direct: the polyhedra domain is not practical for general-purpose static analysis of real-world code. PolyhedralPussycat's B06 (PID controller, 12 vars) and B07 (LZW, 18 vars) both timed out. These are not corner cases — a PID controller is about as idiomatic embedded control code as it gets.

Here's the real problem. It's not just Chernikova's algorithm. The widening story is also broken. The Cousot-Halbwachs widening for convex polyhedra works by retaining only the constraints from the current approximation that were already present (or equivalent to ones that were) in the previous iteration. This guarantees finite convergence, but:

  -- Standard C&H widening on polyhedra:
  P ∇ Q = { c ∈ C(Q) | c ∈ C(P) or C(P) ⊨ c }
  
  Problem: the widening operator can be "too aggressive"
  throwing away constraints that were informative.
  
  Result: the fixpoint we converge to is often far coarser
  than necessary, causing massive false alarm inflation
  AFTER paying the exponential cost to get there.

The precision numbers in PolyhedralPussycat's table look great because they only show the benchmarks that finished. On a real analyzer workload, polyhedra will timeout or OOM on 40-60% of your programs. The "14 non-trivial invariants" on B10 are lovely but meaningless if your CI pipeline is sitting at a wall for 92 seconds per analysis run.

See my longer rant: The polyhedra research-practice gap (megathread).

Alright, I'm going to try to play mediator here before this devolves into the usual GaloisCat vs FixpointFeline thunderdome. Both of you have valid points and I think the disagreement is partly definitional.

The domain hierarchy (for those following along at home):

  Intervals ⊑ Zones ⊑ Octagons ⊑ Polyhedra
      ↑           ↑         ↑            ↑
   O(n)         O(n²)     O(n³)      exp(n)
   fastest     fast       sweet spot  slowest
   imprecise   okay       good        most precise

The octagon domain — constraints of the form ±x ± y ≤ c — sits in a genuinely interesting sweet spot. O(n³) closure cost via Floyd-Warshall-style algorithms, far more expressive than intervals, handles the vast majority of loop invariants that actually matter in practice. Mine's 2006 paper on the octagon abstract domain is required reading for anyone in this debate.

FixpointFeline is correct that for general-purpose production analysis, octagons with a good variable-packing heuristic beat full polyhedra almost every time. GaloisCat is also correct that for specific, carefully-scoped analyses (formal verification of safety-critical code, small procedure summaries, etc.), full polyhedra with decomposition can be worth it.

The issue isn't "polyhedra vs. octagons." It's knowing when to deploy which tool. Some considerations:

On the widening question that FixpointFeline raised: yes, the Cousot-Halbwachs widening is the standard, but Bagnara et al. published "Precise Widening Operators for Convex Polyhedra" which addresses exactly the coarsening problem. You don't have to use the original widening; the PPL actually ships multiple options. See the widening operators megathread for a comparison.

Can I ask a possibly dumb question? In PolyhedralPussycat's setup: which PPL operations are actually dominating the runtime? Because there are multiple expensive pieces here and I'm not sure which is the bottleneck:

  1. Chernikova conversion (H-rep ↔ V-rep)
  2. Join (convex hull) — expensive in H-rep
  3. Meet (intersection) — cheap in H-rep, expensive in V-rep
  4. Project (existential quantification / variable elimination)
  5. Widening step itself

The reason I ask is that depending on your program structure, the bottleneck changes. For loop-heavy code, you're hitting join at every iteration + widening. For procedure calls, projection dominates (computing summaries). For conditional-heavy code, meet is frequent.

Did you profile which operation accounts for the most wall time? The PPL has instrumentation hooks for this.

Great question! Yes, I have the gprof data. Here's the breakdown for the worst performers:

So the culprit is: Chernikova conversion + convex hull, together accounting for 70-80% of runtime. This matches the theoretical expectation. Every join requires computing the convex hull of two polyhedra in V-representation, which then needs converting back to H-representation for the next constraint operation. It's the conversion that kills you.

I tried this! Manually partitioned B03's variables into {error, integral, derivative} vs {setpoint, output, feedback} clusters. Got the runtime down from 14.3s to 2.1s — a 6.8× speedup — without losing any of the invariants that mattered. The polyhedra just stayed in their respective subspaces and never needed joint Chernikova conversion. So GaloisCat is absolutely right about decomposition.

The problem is: how do you automate this partitioning? You'd need to run a pre-analysis to determine the variable dependency graph, then partition — and that pre-analysis itself has a cost. I'll spin up a separate thread about automated variable clustering: Automated variable clustering for polyhedra analysis.

This is mostly true, but I'd note that Astrée does use polyhedral-style reasoning in specific subdomains for safety-critical real-time code (embedded flight software etc.). The trick is they don't run it on the whole program — they scope it to individual procedures with small variable sets. That seems like the right engineering answer tbh.

The profiling data confirms what I expected. 80% of time in Chernikova + hull — exactly the operations that are exponential in theory and blow up in practice.

I want to put a specific number on what "exponential in n variables" means empirically. Based on my own benchmarking (different programs but similar methodology):

The number of generators grows roughly as the Catalan number / McMullen's upper bound — it's combinatorial explosion. Each doubling of variable count roughly squares the cost. This is not a constant factor you can engineer away.

I've read the Bagnara et al. paper. The more precise widening operators they describe are more expensive than the standard C&H widening, not less. You pay more time for more precision. Great for verification of small, critical loops — not helpful when you're already timing out.

Bottom line: polyhedra is a precision tool, not a scalability tool. Use it accordingly. Octagons are the practical workhorse. This isn't a failure of polyhedra — it's a scope mismatch.

I'll actually give GaloisCat partial credit on the decomposition point. If your analysis can automatically identify independent variable clusters BEFORE running polyhedra, decomposed polyhedra is genuinely useful. But that automatic partitioning is a research problem in itself. See PolyhedralPussycat's thread.

Fine, FixpointFeline, you've talked me into a partial concession. The scalability ceiling is real and the numbers in your table above are stark.

But I want to make a different argument for why polyhedra research still matters even if it's not your CI workhorse:

1. Polyhedra as an oracle for weaker domain design. When you design a new, cheaper abstract domain (octagons, pentagons, zones), you validate its precision by comparing against polyhedra on small programs. Polyhedra provides the "ground truth" for what relational information actually exists in a program. Without it, you're flying blind on precision evaluation.

2. Polyhedra for interprocedural summaries. If you compute polyhedral summaries at the function level (functions with small argument count — say ≤8 params), the analysis cost is bounded by the number of parameters, not the program size. This is actually practical! You can then use these precise summaries during a whole-program interval or octagon analysis to propagate relational information across call boundaries without paying exponential costs globally.

3. ELINA is genuinely good. The decomposed polyhedra in ELINA (ETH Library for Numerical Analysis) achieves near-octagon speeds on many programs while retaining polyhedral precision for variable clusters that need it. PolyhedralPussycat, did you try ELINA instead of raw PPL for your timing-out benchmarks?

First post in this thread! Sorry if this is a noob question but I'm a bit lost on one thing. Can someone explain what the Chernikova algorithm is actually doing conceptually? I know it converts between constraint and generator representations but I don't understand why you need both representations in the first place.

Like... can't you just always use constraints (H-representation)?

Great question! Welcome to the forum 🐱. Short answer: some operations are cheap in one representation and expensive in the other. Here's the breakdown:

So yes, you can use only H-representation — this is what the Verimag Polyhedra Library does. The cost is that convex hull (join) becomes your bottleneck via Fourier-Motzkin elimination, which generates many redundant constraints. The PPL instead maintains both representations lazily and converts between them as needed. The conversion is Chernikova's algorithm.

Think of it like always needing both a recipe (constraints: what rules must hold) and a list of extreme points (generators: what combinations are achievable). Some cooking questions are easier with the recipe, some with the list of ingredients.

For a deeper dive: the Double Description Method wiki article and the Chernikova Algorithm explained thread.

Yes, I ran ELINA overnight! Updated results for the tricky benchmarks:

So ELINA decomposed polyhedra is a genuine win for most programs. B09 is the true pathological case — a dense 6×6 Gaussian elimination involves all 40 variables in a fully coupled invariant, so there's nothing to decompose. For this particular program, I don't think any polyhedral analysis is going to work short of dramatic mathematical breakthroughs.

Tentative conclusions (subject to revision as the thread continues):

1. Raw PPL polyhedra: practical for ≤15 relational variables, impractical beyond that.
2. ELINA decomposed polyhedra: practical for ≤25 relational variables IF the dependency graph is sparse.
3. Octagons: practical for arbitrary-size programs; best precision-performance tradeoff for general analysis.
4. Dense fully-coupled programs (Gaussian elimination style): currently nothing beats intervals for scalability, though you pay a precision price.

Thanks everyone for the great discussion. This thread has been way more informative than I expected. Will update with more benchmarks as I run them. 🐾