Polynomial Invariants for Affine Programs

TL;DR

This paper presents an algorithm to compute the strongest polynomial invariants for affine programs, leveraging algebraic methods to analyze the semigroup generated by rational matrices.

Contribution

It introduces a novel algebraic approach to determine polynomial invariants in affine programs, including a method to compute the Zariski closure of matrix semigroups.

Findings

Algorithm computes strongest polynomial invariants at each program location.

Provides a method to compute Zariski closure of matrix semigroups.

Advances algebraic analysis of affine program behaviors.

Abstract

We exhibit an algorithm to compute the strongest polynomial (or algebraic) invariants that hold at each 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.