Conference item icon

Conference item

Porous invariants

Abstract:
We introduce the notion of porous invariants for multipath (or branching/nondeterministic) affine loops over the integers; these invariants are not necessarily convex, and can in fact contain infinitely many ‘holes’. Nevertheless, we show that in many cases such invariants can be automatically synthesised, and moreover can be used to settle (non-)reachability questions for various interesting classes of affine loops and target sets.
Publication status:
Published
Peer review status:
Peer reviewed

Actions


Access Document


Files:
Publisher copy:
10.1007/978-3-030-81688-9_8

Authors


More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Oxford college:
Green Templeton College
Role:
Author
Publisher:
Springer Nature
Host title:
Proceedings of the 33rd International Conference on Computer Aided Verification (CAV 2021)
Series:
Lecture Notes in Computer Science
Volume:
12760
Pages:
172-194
Publication date:
2021-07-15
Event title:
33rd International Conference on Computer Aided Verification (CAV 2021)
Event location:
Online
Event website:
http://i-cav.org/2021/
Event start date:
2021-07-20
Event end date:
2021-07-23
DOI:
EISSN:
1611-3349
ISSN:
0302-9743
ISBN:
978-3-030-81687-2
Language:
English
Keywords:
Pubs id:
1198938
Local pid:
pubs:1198938
Deposit date:
2021-10-11

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