Algebraic Invariants for Affine Programs

ABSTRACT. Automatically generating invariants is a fundamental challenge in program analysis and verification. In this talk we give a select oveview of previous work on this problem, starting with Michael Karr's 1976 algorithm for computing affine invariants in affine programs (i. e. , programs having only non-deterministic (as opposed to conditional) branching and all of whose assignments are given by affine expressions). We then present the central result of the talk---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.

Authors

• James Worrell

Keywords

No keywords are indexed for this paper.