Publication Details

Fast Acceleration of Ultimately Periodic Relations

BOZGA Marius, IOSIF Radu and KONEČNÝ Filip. Fast Acceleration of Ultimately Periodic Relations. In: Computer Aided Verification. Lecture Notes in Computer Science, vol. 6174. Berlin: Springer Verlag, 2010, pp. 227-242. ISBN 978-3-642-14294-9.
Czech title
Akcelerace periodických relací
Type
conference paper
Language
english
Authors
Bozga Marius (VERIMAG)
Iosif Radu (VERIMAG)
Konečný Filip, Ing. (DITS FIT BUT)
URL
Keywords

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

Abstract

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.

Published
2010
Pages
227-242
Proceedings
Computer Aided Verification
Series
Lecture Notes in Computer Science
Volume
6174
Conference
22nd International Conference on Computer-Aided Verification, Edinburgh, GB
ISBN
978-3-642-14294-9
Publisher
Springer Verlag
Place
Berlin, DE
BibTeX
@INPROCEEDINGS{FITPUB9278,
   author = "Marius Bozga and Radu Iosif and Filip Kone\v{c}n\'{y}",
   title = "Fast Acceleration of Ultimately Periodic Relations",
   pages = "227--242",
   booktitle = "Computer Aided Verification",
   series = "Lecture Notes in Computer Science",
   volume = 6174,
   year = 2010,
   location = "Berlin, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-642-14294-9",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/9278"
}
Back to top