Polynomial Invariants for Affine Programs

被引：34

作者：

Hrushovski, Ehud ^{[1
]}

Ouaknine, Joel ^{[2
,3
]}

Pouly, Amaury ^{[2
]}

Worrell, James ^{[3
]}

机构：

[1] Univ Oxford, Math Inst, Oxford, England

[2] Max Planck Inst Software Syst, Saarland Informat Campus, Saarbrucken, Germany

[3] Univ Oxford, Dept Comp Sci, Oxford, England

来源：

LICS'18: PROCEEDINGS OF THE 33RD ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE | 2018年

基金：

英国工程与自然科学研究理事会;

关键词：

D O I：

10.1145/3209108.3209142

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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.

引用

页码：530 / 539

页数：10

共 41 条

[1]

Almagor S., 2018, 45 INT C AUT LANG PR

[2]

[Anonymous], 1988, New Advances in Transcendence Theory

[3]

[Anonymous], 2007, The calculus of computation: decision procedures with applications to verification

[4]

Babai L, 1996, PROCEEDINGS OF THE SEVENTH ANNUAL ACM-SIAM SYMPOSIUM ON DISCRETE ALGORITHMS, P498