Detail publikačního výsledku

Fast Acceleration of Ultimately Periodic Relations

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

Originální název

Fast Acceleration of Ultimately Periodic Relations

Anglický název

Fast Acceleration of Ultimately Periodic Relations

Druh

Stať ve sborníku mimo WoS a Scopus

Originální abstrakt

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.

Anglický abstrakt

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.

Klíčová slova

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

Klíčová slova v angličtině

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

Autoři

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

Rok RIV

2012

Vydáno

09.07.2010

Nakladatel

Springer Verlag

Místo

Berlin

ISBN

978-3-642-14294-9

Kniha

Computer Aided Verification

Edice

Lecture Notes in Computer Science

Svazek

6174

Strany od

227

Strany do

242

Strany počet

15

URL

https://www.fit.vut.cz/research/publication/9278/

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/"
}