Abstract for the talk on 04.07.2018 (09:00 h)Seminar on Nonlinear Algebra
James Worrell (University of Oxford)
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.