Detail publikace

A Verification Toolkit for Numerical Transition Systems

KONEČNÝ Filip, HOJJAT Hossein, IOSIF Radu, KUNCAK Viktor, RUMMER Philipp a GARNIER Florent. A Verification Toolkit for Numerical Transition Systems. Lecture Notes in Computer Science, roč. 2012, č. 7436, s. 247-251. ISSN 0302-9743.
Název česky
Toolkit pro verifikaci numerických přechodivých systémů
Typ
článek v časopise
Jazyk
angličtina
Autoři
Konečný Filip, Ing. (UITS FIT VUT)
Hojjat Hossein (EPFL)
Iosif Radu (VERIMAG)
Kuncak Viktor (EPFL)
Rummer Philipp (Uppsala)
Garnier Florent (VERIMAG)
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{FITPUB10040,
   author = "Filip Kone\v{c}n\'{y} and Hossein Hojjat and Radu Iosif and Viktor Kuncak and Philipp Rummer and Florent Garnier",
   title = "A Verification Toolkit for Numerical Transition Systems",
   pages = "247--251",
   booktitle = "Proceedings of FM'12",
   journal = "Lecture Notes in Computer Science",
   volume = 2012,
   number = 7436,
   year = 2012,
   publisher = "Springer Verlag",
   ISSN = "0302-9743",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/10040"
}
Nahoru