FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Polynomial Invariants for Affine Programs

Authors: Ehud Hrushovski, Joel Ouaknine, Amaury Pouly and James Worrell

Paper Information

Title:Polynomial Invariants for Affine Programs
Authors:Ehud Hrushovski, Joel Ouaknine, Amaury Pouly and James Worrell
Proceedings:LICS PDF files
Editors: Anuj Dawar and Erich Grädel
Keywords:Program invariant, Program analysis, Matrix semigroups, Zariski topology, Algebraic geometry
Abstract:

ABSTRACT. We exhibit an algorithm to compute the strongest polynomial (or algebraic) invariants that hold at each program location of a given affine program (i.e., a program having only non-deterministic (as opposed to conditional) branching, and all of whose assignments are given by affine expressions). 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.

Pages:10
Talk:Jul 10 10:00 (Session 53B)
Paper: