Journal title
LICS '18 Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science
DOI
10.1145/3209108.3209142
Last updated
2024-03-27T09:35:42.7+00:00
Page
530-539
Abstract
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.
Symplectic ID
842302
Submitted to ORA
On
Favourite
Off
Publication type
Conference Paper
ISBN-13
9781450355834
Publication date
09 Jul 2018