Detail publikace
A Verification Toolkit for Numerical Transition Systems
Hojjat Hossein (EPFL)
Iosif Radu (VERIMAG)
Kuncak Viktor (EPFL)
Rummer Philipp (Uppsala)
Garnier Florent (VERIMAG)
Č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.
@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" }