Detail publikace

A Verification Toolkit for Numerical Transition Systems

KONEČNÝ, F.; HOJJAT, H.; IOSIF, R.; KUNCAK, V.; RUMMER, P.; GARNIER, F. A Verification Toolkit for Numerical Transition Systems. Lecture Notes in Computer Science, 2012, vol. 2012, no. 7436, p. 247-251. ISSN: 0302-9743.
Název česky
Toolkit pro verifikaci numerických přechodivých systémů
Typ
článek v časopise
Jazyk
anglicky
Autoři
Konečný Filip, Ing., Ph.D.
Hojjat Hossein
Radu Iosif
Kuncak Viktor
Rummer Philipp
Garnier Florent
Klíčová slova

integer programs, numerical transition systems, verification, acceleration, predicate abstraction

Abstrakt

Článek představuje toolkit a sadu testovacích modelů pro rigorózní verifikaci celočíselných numerických přechodových systémů (INTS), které lze chápat jako grafy toku řízení, jejichž hrany jsou anotovány formulemi v Presbugerově aritmetice. Presentujeme dva nástroje pro verifikaci těchto systémů: FLATA a ELDARICA. FLATA je nástroj založený na přesné akceleraci prřechodových relací. ELDARICA je nástroj založený na predikátové abstrakci s interpolací, který použává teorém prover PRINCESS jako korektní a úplný interpolační prover pro Presburgerovu aritmetiku. Oba nástroje dokáží verifikovat příklady, na nichž předchozí metody selhávaly a představují užitečný výchozí bod pro verifikaci programů s celočíselnými daty. Infrastruktura INTS je veřejně dostupná; doufáme, že podnítí další výzkum, porovnávání verifikačních nástrojů, verifikační soutěže a vzájemně prospěšné propojování odlišných verifikačních metod.

Rok
2012
Strany
247–251
Časopis
Lecture Notes in Computer Science, roč. 2012, č. 7436, ISSN 0302-9743
Kniha
Proceedings of FM'12
Vydavatel
Springer Verlag
BibTeX 
@article{BUT96983,
  author="Filip {Konečný} and Hossein {Hojjat} and Iosif {Radu} and Viktor {Kuncak} and Philipp {Rummer} and Florent {Garnier}",
  title="A Verification Toolkit for Numerical Transition Systems",
  journal="Lecture Notes in Computer Science",
  year="2012",
  volume="2012",
  number="7436",
  pages="247--251",
  issn="0302-9743"
}
Nahoru