Detail publikace

Fast Acceleration of Ultimately Periodic Relations

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

Originální název

Fast Acceleration of Ultimately Periodic Relations

Typ

článek ve sborníku mimo WoS a Scopus

Jazyk

angličtina

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.

Klíčová slova

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

Autoři

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

Rok RIV

2010

Vydáno

9. 7. 2010

Nakladatel

Springer Verlag

Místo

Berlin

ISBN

978-3-642-14294-9

Kniha

Computer Aided Verification

Edice

Lecture Notes in Computer Science

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