SCIENCE@home

On Strongest Algebraic Program Invariants

E. Hrushovski,Joël Ouaknine,Amaury Pouly,J. Worrell

Published 2023 in Journal of the ACM

ABSTRACT

A polynomial program is one in which all assignments are given by polynomial expressions and in which all branching is nondeterministic (as opposed to conditional). Given such a program, an algebraic invariant is one that is defined by polynomial equations over the program variables at each program location. Müller-Olm and Seidl have posed the question of whether one can compute the strongest algebraic invariant of a given polynomial program. In this article, we show that, while strongest algebraic invariants are not computable in general, they can be computed in the special case of affine programs, that is, programs with exclusively linear assignments. For the latter result, 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.

PUBLICATION RECORD

  • Publication year

    2023

  • Venue

    Journal of the ACM

  • Publication date

    2023-08-08

  • Fields of study

    Mathematics, Computer Science

  • Identifiers
    DOI 10.1145/3614319
  • External record

    Open on Semantic Scholar

  • Source metadata

    Semantic Scholar

CITATION MAP

EXTRACTION MAP

CLAIMS

  • No claims are published for this paper.

CONCEPTS

  • No concepts are published for this paper.

REFERENCES

Showing 1-45 of 45 references · Page 1 of 1

CITED BY

Showing 1-23 of 23 citing papers · Page 1 of 1