Conference item icon

Conference item

Polynomial invariants for affine programs

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.
Publication status:
Published
Peer review status:
Peer reviewed

Actions


Access Document


Files:
Publisher copy:
10.1145/3209108.3209142

Authors


More by this author
Institution:
University of Oxford
Division:
MPLS Division
Department:
Mathematical Institute
Role:
Author
More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Oxford college:
St John's College
Role:
Author
More by this author
Institution:
University of Oxford
Division:
MPLS Division
Department:
Computer Science
Role:
Author
Publisher:
Association for Computing Machinery Publisher's website
Journal:
ACM/IEEE Symposium on Logic in Computer Science (LICS) 2018 Journal website
Pages:
530-539
Host title:
LICS '18 Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science
Publication date:
2018-07-09
Acceptance date:
2018-01-19
Event location:
Oxford, UK
DOI:
Source identifiers:
842302
ISBN:
9781450355834
Pubs id:
pubs:842302
UUID:
uuid:a0ede316-9a1d-40f7-8a3b-02eae1520e56
Local pid:
pubs:842302
Deposit date:
2018-04-19

Terms of use


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP