Detail publikace

Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata

HOLÍK, L.; JONSSON, B.; LENGÁL, O.; VOJNAR, T.; TRINH, Q.; ABDULLA, P. Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. Proceedings of ATVA'13. Heidelberg: Springer Verlag, 2013. p. 224-239. ISBN: 978-3-319-02443-1.
Název česky
Použití rozšířených lesních automatů pro verifikaci programů manipulujících s haldou s uspořádáním nad datovými elementy
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Holík Lukáš, doc. Mgr., Ph.D. (UITS)
Jonsson Bengt
Lengál Ondřej, Ing., Ph.D. (UITS)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
Trinh Quy Cong
Abdulla Parosh
Klíčová slova

forest automata, shape analysis, dynamic linked data structures,tree automata, abstraction

Abstrakt

Tento text prezentuje obecný rámec pro verifikaci programů s komplexními dynamickými strukturami, jejichž správnost záleží na relaci uspořádání mezi uloženými datovými strukturami. Náš rámec je založen na pojmu lesního automatu jenž dříve vyvinut pro verifikaci programů manipulujících s haldou. V tomto textu rozšiřujeme lesní automaty o omezení mezi datovými elementy přidruženými k uzlům hald reprezentovaných lesními automaty, a navrhujeme nezbytné úpravy všech operací nezbytných pro použití rozšířených lesních automatů v plně automatickém přístupu k verifikaci, jenž je založen na abstraktní interpretaci. Náš přístup jsme implementovali jako rozšíření nástroje Forester, a aplikovali ho na množství programů manipulujících datové struktury, jako jsou různé varianty jednosměrně a dvojsmerně vázaných seznamů, binární vyhledávací stromy, i přeskakované seznamy. Experimenty ukazují, že náš přístup je nejen plně automatický a relativně obecný, ale také efektivní.

Rok
2013
Strany
224–239
Sborník
Proceedings of ATVA'13
ISBN
978-3-319-02443-1
Vydavatel
Springer Verlag
Místo
Heidelberg
BibTeX 
@inproceedings{BUT103527,
  author="Lukáš {Holík} and Bengt {Jonsson} and Ondřej {Lengál} and Tomáš {Vojnar} and Quy Cong {Trinh} and Parosh {Abdulla}",
  title="Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata",
  booktitle="Proceedings of ATVA'13",
  year="2013",
  pages="224--239",
  publisher="Springer Verlag",
  address="Heidelberg",
  isbn="978-3-319-02443-1"
}
Nahoru