Generating Polynomial Program Invariants

  • James Worrell (University of Oxford)
G3 10 (Lecture hall)


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.

Mirke Olschewski

MPI for Mathematics in the Sciences Contact via Mail

Upcoming Events of This Seminar