Conference paperBOZGA Marius, IOSIF Radu and KONEČNÝ Filip. Fast Acceleration of Ultimately Periodic Relations. In: Computer Aided Verification. Berlin: Springer Verlag, 2010, pp. 227242. ISBN 9783642142949.  Publication language:  english 

Original title:  Fast Acceleration of Ultimately Periodic Relations 

Title (cs):  Akcelerace periodických relací 

Pages:  227242 

Proceedings:  Computer Aided Verification 

Conference:  22nd International Conference on ComputerAided Verification 

Series:  Lecture Notes in Computer Science 6174 

Place:  Berlin, DE 

Year:  2010 

ISBN:  9783642142949 

Publisher:  Springer Verlag 

URL:  http://www.fit.vutbr.cz/~ikonecny/pubs/CAV10.pdf [PDF] 

URL:  http://www.fit.vutbr.cz/~ikonecny/pubs/CAV10.ps [PS] 

Keywords 

acceleration, counter systems, difference bounds relations, octagonal relations, finite monoid affine relations 
Annotation 

Computing transitive closures of integer relations is the key to finding precise
invariants of integer programs. In this paper, we describe an efficient
algorithm for computing the transitive closures of difference bounds,
octagonal and finite monoid affine relations. On the theoretical side,
this framework provides a common solution to the acceleration problem,
for all these three classes of relations. In practice, according to our
experiments, the new method performs up to four orders of magnitude
better than the previous ones, making it a promising approach for the
verification of integer programs.

BibTeX: 

@INPROCEEDINGS{
author = {Marius Bozga and Radu Iosif and Filip Konečný},
title = {Fast Acceleration of Ultimately Periodic Relations},
pages = {227242},
booktitle = {Computer Aided Verification},
series = {Lecture Notes in Computer Science 6174},
year = {2010},
location = {Berlin, DE},
publisher = {Springer Verlag},
ISBN = {9783642142949},
language = {english},
url = {http://www.fit.vutbr.cz/research/view_pub.php.en?id=9278}
} 
