Polynomial Invariants for Affine Programs
Authors: Ehud Hrushovski, Joel Ouaknine, Amaury Pouly and James Worrell
Paper Information
| Title: | Polynomial Invariants for Affine Programs |
| Authors: | Ehud Hrushovski, Joel Ouaknine, Amaury Pouly and James Worrell |
| Proceedings: | LICS PDF files |
| Editors: | Anuj Dawar and Erich Grädel |
| Keywords: | Program invariant, Program analysis, Matrix semigroups, Zariski topology, Algebraic geometry |
| Abstract: | ABSTRACT. We exhibit an algorithm to compute the strongest polynomial (or algebraic) invariants that hold at each program location of a given affine program (i.e., a program having only non-deterministic (as opposed to conditional) branching, and all of whose assignments are given by affine expressions). Our main tool is an algebraic result of independent interest: given a finite set of rational square matrices of the same dimension, we show how to compute the Zariski closure of the semigroup that they generate. |
| Pages: | 10 |
| Talk: | Jul 10 10:00 (Session 53B) |
| Paper: | ![]() |
