Generating Polynomial Program Invariants

Automated invariant generation is a fundamental challenge in program analysis and verification, with work going back several decades. In this talk I will present a select overview and survey of previous work on this problem, and I will describe a new algorithm to compute all polynomial invariants for the class of so-called affine programs (programs that allow affine assignments and non-deterministic branching). Our main technical contribution is a mathematical result of independent interest: an algorithm to compute the Zariski closure of a finitely generated matrix semigroup.

This is joint work with Ehud Hrushovski, Joel Ouaknine, and Amaury Pouly.