Automatically generating invariants is a fundamental challenge in program analysis and verification. In this talk we give a select overview of previous work on this problem, starting with Michael Karr's 1976 algorithm for computing affine invariants for affine programs (i.e., programs in which all assignments are affine and which conditionals are abstracted by non-determinism) and proceeding to subsequent work on computing polynomial invariants for affine programs. We then present our main result-an algorithm to compute all polynomial invariants that hold at each location of a given a affine program. 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. This is joint work with Ehud Hrushovski, Joel Ouaknine, and Amaury Pouly.
17 May 2018, 10h3012h00
Salle de réunion du bâtiment modulaire BP5 (en bas de la BU), Luminy