Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis
summary
Generates loop summaries that abstractions arbitrary loop bodies into a solvable polynomial ideal and then applies a proven complete solver (a generalization of Cowers and Zimmerman) to extract all polynomial invariants of that abstraction. Claims a formal monotonicity guarantee: stronger loop-body information yields stronger summaries. Implements the algorithms, evaluates on SV-COMP suites, reports competitive results and leadership on nonlinear benchmarks, with total runs around 1,130s and 1,750s for two benchmark classes. Artifacts available.
AI-written summary · about
chapters (11)
- 0:00Solvable polynomial ideals intro
- 1:29Prior work on polynomial analysis
- 3:35Compositional summary generation
- 4:38Loop analysis with overapproximation
- 5:41Monotonicity guarantee
- 6:23Solvable polynomial ideals role
- 7:48Step-by-step example
- 10:41Monotonicity enabling features
- 12:07Method overview
- 13:29Benchmark results
- 13:51Q&A