Detail výsledku

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.
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Bozga Marius
Radu Iosif
Konečný Filip, Ing., Ph.D., UITS (FIT)
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

URL
Rok
2010
Strany
227–242
Sborník
Computer Aided Verification
Řada
Lecture Notes in Computer Science
Svazek
6174
Konference
22nd International Conference on Computer-Aided Verification
ISBN
978-3-642-14294-9
Vydavatel
Springer Verlag
Místo
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/"
}
Projekty
Automaty a logiky v symbolické verifikaci software, MŠMT, KONTAKT, MEB021023, zahájení: 2010-01-01, ukončení: 2011-12-31, ukončen
Bezpečné, spolehlivé a adaptivní počítačové systémy, VUT, Vnitřní projekty VUT, FIT-S-10-1, zahájení: 2010-03-01, ukončení: 2010-12-31, ukončen
Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů, GAČR, Doktorské granty, GD102/09/H042, zahájení: 2009-01-30, ukončení: 2012-12-31, ukončen
Pokročilé formální přístupy v návrhu a automatické verifikaci počítačových systémů, GAČR, Standardní projekty, GA102/07/0322, zahájení: 2007-01-01, ukončení: 2009-12-31, ukončen
Práce se složitými datovými strukturami a paralelismem v prostředí Rich Model Toolkit, MŠMT, COST, OC10009, zahájení: 2010-01-01, ukončení: 2012-12-31, řešení
Statická a dynamická verifikace programů s pokročilými rysy paralelismu a neomezenosti, GAČR, Standardní projekty, GAP103/10/0306, zahájení: 2010-01-01, ukončení: 2013-12-31, řešení
Výzkum informačních technologií z hlediska bezpečnosti, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, zahájení: 2007-01-01, ukončení: 2013-12-31, řešení
Výzkumné skupiny
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)
Pracoviště
Ústav inteligentních systémů (UITS)
Nahoru