Detail publikace

Accelerating Interpolants

IOSIF, R.; HOJJAT, H.; KONEČNÝ, F.; KUNCAK, V.; RUMMER, P. Accelerating Interpolants. Lecture Notes in Computer Science, 2012, vol. 2012, no. 7561, p. 187-202. ISSN: 0302-9743.
Název česky
Akcelerované interpolanty
Typ
článek v časopise
Jazyk
anglicky
Autoři
Radu Iosif
Hojjat Hossein
Konečný Filip, Ing., Ph.D.
Kuncak Viktor
Rummer Philipp
Klíčová slova

integer programs, verification, reachability analysis, acceleration, predicate abstraction, interpolation

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{BUT97017,
  author="Iosif {Radu} and Hossein {Hojjat} and Filip {Konečný} and Viktor {Kuncak} and Philipp {Rummer}",
  title="Accelerating Interpolants",
  journal="Lecture Notes in Computer Science",
  year="2012",
  volume="2012",
  number="7561",
  pages="187--202",
  issn="0302-9743"
}
Nahoru