Detail publikace

Accelerating Interpolants

IOSIF Radu, HOJJAT Hossein, KONEČNÝ Filip, KUNCAK Viktor a RUMMER Philipp. Accelerating Interpolants. Lecture Notes in Computer Science, roč. 2012, č. 7561, s. 187-202. ISSN 0302-9743.
Název česky
Akcelerované interpolanty
Typ
článek v časopise
Jazyk
angličtina
Autoři
Iosif Radu (VERIMAG)
Hojjat Hossein (EPFL)
Konečný Filip, Ing. (UITS FIT VUT)
Kuncak Viktor (EPFL)
Rummer Philipp (Uppsala)
Abstrakt

Práce představuje Counterexample-Guided Accelerated Abstraction Refinement (CEGAAR), nový algoritmus pro verifikaci nekonečně stavových systémů. CEGAAR kombinuje predikátovou abstrakci založenou na objevování predikátů pomocí interpolace s akceleračními technikami pro výpočet tranzitivních uzávěrů cyklů programu. CEGAAR aplikuje akceleraci k dynamickému detekování cyklů v rozvinutém přechodobém systému a kombinuje nadaproximaci s podaproximací. CEGAAR konstruuje induktivní interpolanty, které vyloučí nekonečnou množinu falešných protipříkladů, čímž se zmírní problém divergence predikítové abstrakce. Teoretickým výsledkem práce je, že induktivní interpolanty lze vypočítat přímo z tradičních Craigových interpolantů a tranzitivních uzávěrů smyček. Práce taktéž představuje výslednou implementaci, která úspěšně verifikuje množství programů, na nichž předchozí přístupy selhávaly.

Rok
2012
Strany
187-202
Časopis
Lecture Notes in Computer Science, roč. 2012, č. 7561, ISSN 0302-9743
Kniha
Proceedings of ATVA'12
Vydavatel
Springer Verlag
BibTeX 
@ARTICLE{FITPUB10102,
   author = "Radu Iosif and Hossein Hojjat and Filip Kone\v{c}n\'{y} and Viktor Kuncak and Philipp Rummer",
   title = "Accelerating Interpolants",
   pages = "187--202",
   booktitle = "Proceedings of ATVA'12",
   journal = "Lecture Notes in Computer Science",
   volume = 2012,
   number = 7561,
   year = 2012,
   publisher = "Springer Verlag",
   ISSN = "0302-9743",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/10102"
}
Nahoru