Polynomial Invariants for Affine Programs

on YouTube ↗32m

" summary

Claims an algorithm that computes a finite basis of all polynomial invariants for affine loops by reducing invariant synthesis to algebraic-geometry problems, specifically computing the Zariski closure of the semigroup generated by the update matrices. Method combines linear-algebra eigen-decomposition with symbolic tools such as Gröbner bases to produce generators of the invariant ideal. Includes a prototype implementation and benchmark runs showing the method terminates and outputs complete algebraic and semi-algebraic invariants for representative affine programs.

AI-written summary · about

" chapters (16)

1. 0:00Intro
2. 0:35Programming in the Jurassic
3. 4:49Why Invariants?
4. 5:49A Problem in Program Analysis
5. 7:52Polynomial Invariants: Geometric Picture
6. 9:36Computing a Strongest Algebraic Invariant
7. 11:15Finding all polynomial invariants
8. 11:36Undecidability
9. 13:32Affine Invariants for Affine Programs
10. 14:37Polynomial Invariants for Affine Programs
11. 15:16Strongest Algebraic Invariants
12. 18:47From Affine Programs to Hybrid Automata
13. 21:21A Challenge in Program Analysis
14. 22:32Semi-Algebraic Invariant Synthesis
15. 29:13Minimal Families of Invariants
16. 29:30The Monniaux Problem