Publication Details

Fast Acceleration of Ultimately Periodic Relations

BOZGA, M.; IOSIF, R.; KONEČNÝ, F. Fast Acceleration of Ultimately Periodic Relations. Computer Aided Verification. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2010. p. 227-242. ISBN: 978-3-642-14294-9.

Czech title

Akcelerace periodických relací

Type

conference paper

Language

English

Authors

Bozga Marius
Radu Iosif
Konečný Filip, Ing., Ph.D.

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

ISBN

978-3-642-14294-9

Publisher

Springer Verlag

Place

Berlin

BibTeX

@inproceedings{BUT34831,
  author="Marius {Bozga} and Iosif {Radu} and Filip {Konečný}",
  title="Fast Acceleration of Ultimately Periodic Relations",
  booktitle="Computer Aided Verification",
  year="2010",
  series="Lecture Notes in Computer Science",
  volume="6174",
  pages="227--242",
  publisher="Springer Verlag",
  address="Berlin",
  isbn="978-3-642-14294-9",
  url="https://www.fit.vut.cz/research/publication/9278/"
}