## Polynomial invariants for affine programs

*Ehud Hrushovski*,
*Joël
Ouaknine*, *Amaury Pouly*,
and *James Worrell*
We exhibit an algorithm to compute the strongest polynomial (or
algebraic) invariants that hold at each 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.

*Proceedings of LICS 18*, 2018. 10 pages.

PDF
© 2018 Association for Computing Machinery.

Imprint / Data Protection