PolyAbs: Parallel Abstract Interpretation for Polynomial Programs with Range Bound Assertions

PolyAbs is a static verification tool for polynomial programs based on abstract interpretation. It proves range-bound assertions (e.g., x ∈ [-20, -4] ∪ [4, 20]) by computing over-approximations of reachable states as powersets of hyper-rectangles (boxes). Key technical contributions include novel abstract transformers and refinement operators that more precisely account for the semantics of polynomial assignments and guards, while supporting parallelization and efficient implementation. This is achieved by leveraging Farkas' Lemma and Handelman's Theorem, and by exploiting geometric properties of unions of hyper-rectangles. The analysis runs in two phases: Phase 1 — Widening: computes a sound over-approximation of the reachable set by iterating the transfer functions with widening until a fixpoint is reached. Phase 2 — Narrowing: refines the result to reduce over-approximation, improving precision without losing soundness.