Detail publikace
Fully Automated Shape Analysis Based on Forest Automata
Lengál Ondřej, Ing., Ph.D. (UITS)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS)
Šimáček Jiří, Ing., Ph.D.
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
Lesní automaty byly v nedávné době navrženy jako nástroj pro analýzu komplexních struktur v haldách programů. Lesní automaty reprezentují množinu stromových dekompozicí grafů haldy ve formě uspořádané množiny stromových automatů. S ohledem na možnost reprezentace složitých datových struktur na haldě umožňoval formalismus lesních automatů uživateli dodat sadu lesních automatů (nazývaných krabice), které reprezentovaly opakující se vzory v grafu haldy, jako symboly jiných lesních automatů vyšší úrovně. V tomto článku navrhujeme inovativní techniku automatického učení se krabic, která umožňuje vyhnout se kroku jejich manuální konstrukce. Dále navrhujeme podstatné vylepšení automatové abstrakce použité v analýze. Výsledkem je efektivní, plně automatizovaná analýza která umožňuje verifikaci i tak složitých datových struktur, jako jsou například přeskakované seznamy. Výkon této analýzy je srovnatelný s nejmodernějšími plně automatizovanými nástroji založenými na separační logice, které jsou však specializované pouze na programy se seznamy.
@techreport{BUT192914,
author="Lukáš {Holík} and Ondřej {Lengál} and Adam {Rogalewicz} and Jiří {Šimáček} and Tomáš {Vojnar}",
title="Fully Automated Shape Analysis Based on Forest Automata",
year="2013",
publisher="Faculty of Information Technology BUT",
address="FIT-TR-2013-01, Brno",
pages="1--25",
url="http://www.fit.vutbr.cz/~ilengal/pub/FIT-TR-2013-01.pdf"
}