James Worrell (University of Oxford)
Wednesday, July 4, 2018 - 09:00
MPI für Mathematik in den Naturwissenschaften Leipzig
Inselstr. 22, 04103 Leipzig, G3 10 (Hörsaal), 3. Etage
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.
submitted by Saskia Gutzschebauch (Saskia.Gutzschebauch@mis.mpg.de, 0341 9959 50)