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
[5]  
Basu S., 2006, Algorithms and Computation in Mathematics
[6]  
Becker T., 1993, GRADUATE TEXTS MATH, V141
[7]   Decidable and undecidable problems about quantum automata [J].
Blondel, VD ;
Jeandel, E ;
Koiran, P ;
Portier, N .
SIAM JOURNAL ON COMPUTING, 2005, 34 (06) :1464-1473
[8]   Inference of polynomial invariants for imperative programs: A farewell to Grobner bases [J].
Cachera, David ;
Jensen, Thomas ;
Jobin, Arnaud ;
Kirchner, Florent .
SCIENCE OF COMPUTER PROGRAMMING, 2014, 93 :89-109
[9]   Polynomial approximations of the relational semantics of imperative programs [J].
Colon, Michael A. .
SCIENCE OF COMPUTER PROGRAMMING, 2007, 64 (01) :76-96
[10]  
Cousot P., 1978, POPL, P84, DOI DOI 10.1145/512760.512770