TY - GEN
T1 - Polynomial invariants for affine programs
AU - Hrushovski, Ehud
AU - Ouaknine, Joël
AU - Pouly, Amaury
AU - Worrell, James
N1 - Publisher Copyright:
© 2018 ACM.
PY - 2018/7/9
Y1 - 2018/7/9
N2 - 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.
AB - 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.
U2 - 10.1145/3209108.3209142
DO - 10.1145/3209108.3209142
M3 - Conference contribution
AN - SCOPUS:85051103141
T3 - Proceedings - Symposium on Logic in Computer Science
SP - 530
EP - 539
BT - Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018
Y2 - 9 July 2018 through 12 July 2018
ER -