Scalable Linear Invariant Generation with Farkas’ Lemma
summary
Generates tight linear invariants for affine programs modeled as linear transition systems using Farkas' Lemma and keeps completeness while removing the original bottleneck. Two concrete engineering changes are implemented: per-location generation that separates and parallelizes invariant search and reduces combinatorial blowup, and segmented subsumption testing during the CNF-to-DNF expansion that finds local subsumptions early. Formal proof preserves accuracy and experiments report runtime improvements by several orders of magnitude even when summed non‑parallel.
AI-written summary · about
chapters (4)
related talks
01h 05mAll the Languages Together
27mDistributing and Parallelizing Non-canonical Loops
01h 22mTutorial 3: Geometric Invariant Theory
16mTowards formally secure compilation of verified F* programs against unverified ML(…)
22mStrong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants f...
22mA Calculus of Inductive Linear Constructions
25mAUTOMAP: Inferring Rank-Polymorphic Function Applications with Integer Linear Programming
33mSolving constraints during type inference