Publication detail

Fast Acceleration of Ultimately Periodic Relations

BOZGA, M. IOSIF, R. KONEČNÝ, F.

Original Title

Fast Acceleration of Ultimately Periodic Relations

English Title

Fast Acceleration of Ultimately Periodic Relations

Type

conference paper

Language

en

Original 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.

English 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.

Keywords

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

RIV year

2010

Released

09.07.2010

Publisher

Springer Verlag

Location

Berlin

ISBN

978-3-642-14294-9

Book

Computer Aided Verification

Edition

Lecture Notes in Computer Science

Edition number

NEUVEDEN

Pages from

227

Pages to

242

Pages count

15

URL

Documents

BibTex


@inproceedings{BUT34831,
  author="Marius {Bozga} and Iosif {Radu} and Filip {Konečný}",
  title="Fast Acceleration of Ultimately Periodic Relations",
  annote="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.",
  address="Springer Verlag",
  booktitle="Computer Aided Verification",
  chapter="34831",
  edition="Lecture Notes in Computer Science",
  howpublished="print",
  institution="Springer Verlag",
  year="2010",
  month="july",
  pages="227--242",
  publisher="Springer Verlag",
  type="conference paper"
}